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

Theorem th3qlem1 6144
Description: Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. (Contributed by NM, 3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
Hypotheses
Ref Expression
th3qlem1.1  .~  Er  S
th3qlem1.3  S  S  S  S  .~  .~  .+  .~  .+
Assertion
Ref Expression
th3qlem1  S /.  .~  S /.  .~  .~  .~  .+  .~
Distinct variable groups:   ,,,,,  .+   ,  .~ ,,,,   , S,,,,   ,,,,,   ,,,,,

Proof of Theorem th3qlem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ee4anv 1806 . . . 4  .~  .~  .+  .~  .~  .~  .+  .~  .~  .~  .+  .~  .~  .~  .+  .~
2 an4 520 . . . . . . 7  .~  .~  .+  .~  .~  .~  .+  .~  .~  .~  .~  .~  .+  .~  .+  .~
3 eleq1 2097 . . . . . . . . . . . . 13  .~  S /.  .~  .~  S /.  .~
4 eleq1 2097 . . . . . . . . . . . . 13  .~  S /.  .~  .~  S /.  .~
53, 4bi2anan9 538 . . . . . . . . . . . 12  .~  .~  S /.  .~  S /.  .~  .~  S /.  .~  .~  S /.  .~
65adantr 261 . . . . . . . . . . 11  .~  .~  .~  .~  S /.  .~  S /.  .~  .~  S /.  .~  .~  S /.  .~
76biimpac 282 . . . . . . . . . 10  S /.  .~  S /.  .~  .~  .~  .~  .~  .~  S /.  .~  .~  S /.  .~
8 eqtr2 2055 . . . . . . . . . . . . 13  .~  .~  .~  .~
9 eqtr2 2055 . . . . . . . . . . . . 13  .~  .~  .~  .~
108, 9anim12i 321 . . . . . . . . . . . 12  .~  .~  .~  .~  .~  .~  .~  .~
1110an4s 522 . . . . . . . . . . 11  .~  .~  .~  .~  .~  .~  .~  .~
1211adantl 262 . . . . . . . . . 10  S /.  .~  S /.  .~  .~  .~  .~  .~  .~  .~  .~  .~
13 th3qlem1.1 . . . . . . . . . . . 12  .~  Er  S
1413a1i 9 . . . . . . . . . . 11  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  Er  S
15 simprl 483 . . . . . . . . . . . . 13  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  .~
16 erdm 6052 . . . . . . . . . . . . . . . 16  .~  Er  S  dom  .~  S
1713, 16ax-mp 7 . . . . . . . . . . . . . . 15  dom  .~  S
18 simpll 481 . . . . . . . . . . . . . . 15  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  S /.  .~
19 ecelqsdm 6112 . . . . . . . . . . . . . . 15  dom  .~  S  .~  S /.  .~  S
2017, 18, 19sylancr 393 . . . . . . . . . . . . . 14  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  S
2114, 20erth 6086 . . . . . . . . . . . . 13  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  .~  .~
2215, 21mpbird 156 . . . . . . . . . . . 12  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~
23 simprr 484 . . . . . . . . . . . . 13  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  .~
24 simplr 482 . . . . . . . . . . . . . . 15  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  S /.  .~
25 ecelqsdm 6112 . . . . . . . . . . . . . . 15  dom  .~  S  .~  S /.  .~  S
2617, 24, 25sylancr 393 . . . . . . . . . . . . . 14  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  S
2714, 26erth 6086 . . . . . . . . . . . . 13  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  .~  .~
2823, 27mpbird 156 . . . . . . . . . . . 12  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~
2915, 18eqeltrrd 2112 . . . . . . . . . . . . . 14  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  S /.  .~
30 ecelqsdm 6112 . . . . . . . . . . . . . 14  dom  .~  S  .~  S /.  .~  S
3117, 29, 30sylancr 393 . . . . . . . . . . . . 13  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  S
3223, 24eqeltrrd 2112 . . . . . . . . . . . . . 14  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  S /.  .~
33 ecelqsdm 6112 . . . . . . . . . . . . . 14  dom  .~  S  .~  S /.  .~  S
3417, 32, 33sylancr 393 . . . . . . . . . . . . 13  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  S
35 th3qlem1.3 . . . . . . . . . . . . 13  S  S  S  S  .~  .~  .+  .~  .+
3620, 31, 26, 34, 35syl22anc 1135 . . . . . . . . . . . 12  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .~  .~  .+  .~  .+
3722, 28, 36mp2and 409 . . . . . . . . . . 11  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .+ 
.~  .+
3814, 37erthi 6088 . . . . . . . . . 10  .~  S /.  .~  .~  S /.  .~  .~  .~  .~  .~  .+  .~  .+  .~
397, 12, 38syl2anc 391 . . . . . . . . 9  S /.  .~  S /.  .~  .~  .~  .~  .~  .+  .~  .+  .~
40 eqeq12 2049 . . . . . . . . 9  .+  .~  .+  .~  .+  .~  .+  .~
4139, 40syl5ibrcom 146 . . . . . . . 8  S /.  .~  S /.  .~  .~  .~  .~  .~  .+  .~  .+  .~
4241expimpd 345 . . . . . . 7  S /.  .~  S /.  .~  .~  .~  .~  .~  .+  .~  .+  .~
432, 42syl5bi 141 . . . . . 6  S /.  .~  S /.  .~  .~  .~  .+  .~  .~  .~  .+  .~
4443exlimdvv 1774 . . . . 5  S /.  .~  S /.  .~  .~  .~  .+  .~  .~  .~  .+  .~
4544exlimdvv 1774 . . . 4  S /.  .~  S /.  .~  .~  .~  .+  .~  .~  .~  .+  .~
461, 45syl5bir 142 . . 3  S /.  .~  S /.  .~  .~  .~  .+  .~  .~  .~  .+  .~
4746alrimivv 1752 . 2  S /.  .~  S /.  .~  .~  .~  .+  .~  .~  .~  .+  .~
48 eqeq1 2043 . . . . . 6  .+  .~  .+  .~
4948anbi2d 437 . . . . 5  .~  .~  .+  .~  .~  .~  .+  .~
50492exbidv 1745 . . . 4  .~  .~  .+  .~  .~  .~  .+  .~
51 eceq1 6077 . . . . . . . 8  .~  .~
5251eqeq2d 2048 . . . . . . 7  .~  .~
53 eceq1 6077 . . . . . . . 8  .~  .~
5453eqeq2d 2048 . . . . . . 7  .~  .~
5552, 54bi2anan9 538 . . . . . 6  .~  .~  .~  .~
56 oveq12 5464 . . . . . . . 8  .+  .+
5756eceq1d 6078 . . . . . . 7  .+  .~  .+  .~
5857eqeq2d 2048 . . . . . 6  .+  .~  .+  .~
5955, 58anbi12d 442 . . . . 5  .~  .~  .+  .~  .~  .~  .+  .~
6059cbvex2v 1796 . . . 4  .~  .~  .+  .~  .~  .~  .+  .~
6150, 60syl6bb 185 . . 3  .~  .~  .+  .~  .~  .~  .+  .~
6261mo4 1958 . 2  .~  .~  .+  .~  .~  .~  .+  .~  .~  .~  .+  .~
6347, 62sylibr 137 1  S /.  .~  S /.  .~  .~  .~  .+  .~
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98  wal 1240   wceq 1242  wex 1378   wcel 1390  wmo 1898   class class class wbr 3755   dom cdm 4288  (class class class)co 5455    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-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
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-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-fv 4853  df-ov 5458  df-er 6042  df-ec 6044  df-qs 6048
This theorem is referenced by:  th3qlem2  6145
  Copyright terms: Public domain W3C validator