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

Theorem th3qlem2 6539
 Description: Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
Hypotheses
Ref Expression
th3q.1
th3q.2
th3q.4
Assertion
Ref Expression
th3qlem2
Distinct variable groups:   ,,,,,,,,,   ,,,,,,,,,   ,,,,,,,   ,,,,,,,   , ,,,,,,,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem th3qlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 th3q.2 . . 3
2 eqid 2140 . . . . 5
3 breq1 3939 . . . . . . . 8
43anbi1d 461 . . . . . . 7
5 oveq1 5788 . . . . . . . 8
65breq1d 3946 . . . . . . 7
74, 6imbi12d 233 . . . . . 6
87imbi2d 229 . . . . 5
9 breq2 3940 . . . . . . . 8
109anbi1d 461 . . . . . . 7
11 oveq1 5788 . . . . . . . 8
1211breq2d 3948 . . . . . . 7
1310, 12imbi12d 233 . . . . . 6
1413imbi2d 229 . . . . 5
15 breq1 3939 . . . . . . . . . 10
1615anbi2d 460 . . . . . . . . 9
17 oveq2 5789 . . . . . . . . . 10
1817breq1d 3946 . . . . . . . . 9
1916, 18imbi12d 233 . . . . . . . 8
2019imbi2d 229 . . . . . . 7
21 breq2 3940 . . . . . . . . . 10
2221anbi2d 460 . . . . . . . . 9
23 oveq2 5789 . . . . . . . . . 10
2423breq2d 3948 . . . . . . . . 9
2522, 24imbi12d 233 . . . . . . . 8
2625imbi2d 229 . . . . . . 7
27 th3q.4 . . . . . . . 8
2827expcom 115 . . . . . . 7
292, 20, 26, 282optocl 4623 . . . . . 6
3029com12 30 . . . . 5
312, 8, 14, 302optocl 4623 . . . 4
3231imp 123 . . 3
331, 32th3qlem1 6538 . 2
34 vex 2692 . . . . . . 7
35 vex 2692 . . . . . . 7
3634, 35opex 4158 . . . . . 6
37 vex 2692 . . . . . . 7
38 vex 2692 . . . . . . 7
3937, 38opex 4158 . . . . . 6
40 eceq1 6471 . . . . . . . . 9
4140eqeq2d 2152 . . . . . . . 8
42 eceq1 6471 . . . . . . . . 9
4342eqeq2d 2152 . . . . . . . 8
4441, 43bi2anan9 596 . . . . . . 7
45 oveq12 5790 . . . . . . . . 9
4645eceq1d 6472 . . . . . . . 8
4746eqeq2d 2152 . . . . . . 7
4844, 47anbi12d 465 . . . . . 6
4936, 39, 48spc2ev 2784 . . . . 5
5049exlimivv 1869 . . . 4
5150exlimivv 1869 . . 3
5251moimi 2065 . 2
5333, 52syl 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wceq 1332  wex 1469   wcel 1481  wmo 2001  cvv 2689  cop 3534   class class class wbr 3936   cxp 4544  (class class class)co 5781   wer 6433  cec 6434  cqs 6435 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-sbc 2913  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-opab 3997  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fv 5138  df-ov 5784  df-er 6436  df-ec 6438  df-qs 6442 This theorem is referenced by:  th3qcor  6540  th3q  6541
 Copyright terms: Public domain W3C validator