ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  th3q Unicode version

Theorem th3q 6147
Description: Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
Hypotheses
Ref Expression
th3q.1  .~  _V
th3q.2  .~  Er  S  X.  S
th3q.4  S  S  S  t  S  s  S  S  S  h  S  <. , 
>.  .~  <. ,  t
>.  <. s , 
>.  .~  <. ,  h >.  <. ,  >.  .+  <. s ,  >.  .~  <. ,  t
>.  .+  <. ,  h >.
th3q.5  G  { <. <. , 
>. ,  >.  |  S  X.  S /.  .~  S  X.  S /.  .~  t  <. ,  >. 
.~  <. ,  t
>.  .~  <. ,  >.  .+ 
<. ,  t >.  .~  }
Assertion
Ref Expression
th3q  S  S  C  S  D  S  <. ,  >.  .~  G <. C ,  D >. 
.~  <. ,  >.  .+  <. C ,  D >.  .~
Distinct variable groups:   ,,,,,, t, s,,, h, 
.~   , S,,,,,, t, s,,, h   ,,,,,,, t, s,   ,,,,,,, t, s,   , C,,,,,, t   , D,,,,,, t   ,  .+ ,,,,,, t, s,,, h
Allowed substitution hints:   (, h)   (, h)    C(,, h, s)    D(,, h, s)    G(,,,,,, t,,, h, s)

Proof of Theorem th3q
StepHypRef Expression
1 opelxpi 4319 . . . 4  S  S  <. ,  >.  S  X.  S
2 th3q.1 . . . . 5  .~  _V
32ecelqsi 6096 . . . 4  <. ,  >.  S  X.  S  <. ,  >.  .~  S  X.  S /.  .~
41, 3syl 14 . . 3  S  S  <. ,  >.  .~  S  X.  S /.  .~
5 opelxpi 4319 . . . 4  C  S  D  S  <. C ,  D >.  S  X.  S
62ecelqsi 6096 . . . 4  <. C ,  D >.  S  X.  S  <. C ,  D >.  .~  S  X.  S /.  .~
75, 6syl 14 . . 3  C  S  D  S  <. C ,  D >.  .~  S  X.  S /.  .~
84, 7anim12i 321 . 2  S  S  C  S  D  S  <. ,  >.  .~  S  X.  S /.  .~ 
<. C ,  D >. 
.~  S  X.  S
/.  .~
9 eqid 2037 . . . 4  <. ,  >.  .~  <. ,  >.  .~
10 eqid 2037 . . . 4  <. C ,  D >.  .~  <. C ,  D >.  .~
119, 10pm3.2i 257 . . 3  <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. C ,  D >. 
.~
12 eqid 2037 . . 3  <. ,  >.  .+ 
<. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~
13 opeq12 3542 . . . . . 6  <. , 
>.  <. ,  >.
14 eceq1 6077 . . . . . . . . 9  <. ,  >.  <. ,  >.  <. ,  >. 
.~  <. ,  >.  .~
1514eqeq2d 2048 . . . . . . . 8  <. ,  >.  <. ,  >.  <. ,  >.  .~  <. ,  >. 
.~  <. ,  >.  .~  <. ,  >. 
.~
1615anbi1d 438 . . . . . . 7  <. ,  >.  <. ,  >.  <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. C ,  D >.  .~  <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. C ,  D >. 
.~
17 oveq1 5462 . . . . . . . . 9  <. ,  >.  <. ,  >.  <. ,  >.  .+ 
<. C ,  D >.  <. ,  >.  .+  <. C ,  D >.
1817eceq1d 6078 . . . . . . . 8  <. ,  >.  <. ,  >.  <. , 
>.  .+  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~
1918eqeq2d 2048 . . . . . . 7  <. ,  >.  <. ,  >.  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~
2016, 19anbi12d 442 . . . . . 6  <. ,  >.  <. ,  >.  <. ,  >.  .~  <. , 
>.  .~  <. C ,  D >. 
.~  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~  <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~
2113, 20syl 14 . . . . 5  <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. C ,  D >. 
.~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. C ,  D >.  .~  <. ,  >.  .~  <. ,  >.  .~  <. C ,  D >. 
.~  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~
2221spc2egv 2636 . . . 4  S  S  <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. C ,  D >. 
.~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .~  <. , 
>.  .~  <. C ,  D >. 
.~  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~
23 opeq12 3542 . . . . . . 7  C  t  D  <. ,  t
>.  <. C ,  D >.
24 eceq1 6077 . . . . . . . . . 10  <. ,  t >.  <. C ,  D >.  <. ,  t >.  .~  <. C ,  D >.  .~
2524eqeq2d 2048 . . . . . . . . 9  <. ,  t >.  <. C ,  D >.  <. C ,  D >.  .~  <. ,  t >.  .~  <. C ,  D >.  .~  <. C ,  D >.  .~
2625anbi2d 437 . . . . . . . 8  <. ,  t >.  <. C ,  D >.  <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. ,  t
>.  .~  <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. C ,  D >. 
.~
27 oveq2 5463 . . . . . . . . . 10  <. ,  t >.  <. C ,  D >.  <. ,  >.  .+ 
<. ,  t >.  <. ,  >.  .+  <. C ,  D >.
2827eceq1d 6078 . . . . . . . . 9  <. ,  t >.  <. C ,  D >.  <. , 
>.  .+  <. ,  t
>.  .~  <. , 
>.  .+  <. C ,  D >.  .~
2928eqeq2d 2048 . . . . . . . 8  <. ,  t >.  <. C ,  D >.  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~  <. , 
>.  .+  <. C ,  D >.  .~
3026, 29anbi12d 442 . . . . . . 7  <. ,  t >.  <. C ,  D >.  <. ,  >.  .~  <. , 
>.  .~  <. C ,  D >. 
.~  <. ,  t >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. ,  t >.  .~  <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. C ,  D >.  .~
3123, 30syl 14 . . . . . 6  C  t  D  <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. ,  t >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~  <. ,  >.  .~  <. , 
>.  .~  <. C ,  D >. 
.~  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~
3231spc2egv 2636 . . . . 5  C  S  D  S  <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. C ,  D >. 
.~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. C ,  D >.  .~  t <. ,  >.  .~  <. , 
>.  .~  <. C ,  D >. 
.~  <. ,  t >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. ,  t >.  .~
33322eximdv 1759 . . . 4  C  S  D  S  <. ,  >.  .~  <. , 
>.  .~  <. C ,  D >. 
.~  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~  t <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. ,  t
>.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~
3422, 33sylan9 389 . . 3  S  S  C  S  D  S  <. ,  >.  .~  <. ,  >.  .~  <. C ,  D >. 
.~  <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~  t <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. ,  t
>.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~
3511, 12, 34mp2ani 408 . 2  S  S  C  S  D  S  t <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. ,  t >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~
36 ecexg 6046 . . . 4  .~  _V  <. ,  >.  .+ 
<. C ,  D >.  .~  _V
372, 36ax-mp 7 . . 3  <. ,  >.  .+ 
<. C ,  D >.  .~  _V
38 eqeq1 2043 . . . . . . . 8  <. ,  >.  .~  <. ,  >. 
.~  <. ,  >.  .~  <. ,  >. 
.~
39 eqeq1 2043 . . . . . . . 8  <. C ,  D >.  .~  <. ,  t >.  .~  <. C ,  D >.  .~  <. ,  t
>.  .~
4038, 39bi2anan9 538 . . . . . . 7  <. ,  >.  .~  <. C ,  D >.  .~  <. ,  >.  .~  <. ,  t >.  .~  <. ,  >.  .~  <. , 
>.  .~  <. C ,  D >. 
.~  <. ,  t >.  .~
41 eqeq1 2043 . . . . . . 7  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+  <. ,  t >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. ,  t >.  .~
4240, 41bi2anan9 538 . . . . . 6  <. ,  >. 
.~  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~  <. , 
>.  .~  <. ,  t
>.  .~  <. ,  >.  .+ 
<. ,  t >.  .~  <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. ,  t
>.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~
43423impa 1098 . . . . 5  <. ,  >.  .~  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~  <. , 
>.  .~  <. ,  t
>.  .~  <. ,  >.  .+ 
<. ,  t >.  .~  <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. ,  t
>.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~
44434exbidv 1747 . . . 4  <. ,  >.  .~  <. C ,  D >.  .~  <. ,  >.  .+ 
<. C ,  D >.  .~  t  <. ,  >. 
.~  <. ,  t
>.  .~  <. ,  >.  .+ 
<. ,  t >.  .~  t <. ,  >. 
.~  <. ,  >.  .~  <. C ,  D >.  .~  <. ,  t >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~
45 th3q.2 . . . . 5  .~  Er  S  X.  S
46 th3q.4 . . . . 5  S  S  S  t  S  s  S  S  S  h  S  <. , 
>.  .~  <. ,  t
>.  <. s , 
>.  .~  <. ,  h >.  <. ,  >.  .+  <. s ,  >.  .~  <. ,  t
>.  .+  <. ,  h >.
472, 45, 46th3qlem2 6145 . . . 4  S  X.  S
/.  .~  S  X.  S /.  .~  t  <. ,  >. 
.~  <. ,  t
>.  .~  <. ,  >.  .+ 
<. ,  t >.  .~
48 th3q.5 . . . 4  G  { <. <. , 
>. ,  >.  |  S  X.  S /.  .~  S  X.  S /.  .~  t  <. ,  >. 
.~  <. ,  t
>.  .~  <. ,  >.  .+ 
<. ,  t >.  .~  }
4944, 47, 48ovig 5564 . . 3  <. ,  >.  .~  S  X.  S /.  .~ 
<. C ,  D >. 
.~  S  X.  S
/.  .~  <. ,  >.  .+  <. C ,  D >.  .~  _V  t <. ,  >.  .~  <. ,  >. 
.~  <. C ,  D >.  .~  <. ,  t
>.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. , 
>.  .+  <. ,  t
>.  .~  <. ,  >.  .~  G <. C ,  D >.  .~  <. ,  >.  .+  <. C ,  D >.  .~
5037, 49mp3an3 1220 . 2  <. ,  >.  .~  S  X.  S /.  .~ 
<. C ,  D >. 
.~  S  X.  S
/.  .~  t <. ,  >.  .~  <. , 
>.  .~  <. C ,  D >. 
.~  <. ,  t >.  .~  <. ,  >.  .+  <. C ,  D >.  .~  <. ,  >.  .+ 
<. ,  t >.  .~  <. ,  >.  .~  G <. C ,  D >. 
.~  <. ,  >.  .+  <. C ,  D >.  .~
518, 35, 50sylc 56 1  S  S  C  S  D  S  <. ,  >.  .~  G <. C ,  D >. 
.~  <. ,  >.  .+  <. C ,  D >.  .~
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   w3a 884   wceq 1242  wex 1378   wcel 1390   _Vcvv 2551   <.cop 3370   class class class wbr 3755    X. cxp 4286  (class class class)co 5455   {coprab 5456    Er wer 6039  cec 6040   /.cqs 6041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fv 4853  df-ov 5458  df-oprab 5459  df-er 6042  df-ec 6044  df-qs 6048
This theorem is referenced by:  oviec  6148
  Copyright terms: Public domain W3C validator