Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aomclem8 Structured version   Unicode version

Theorem aomclem8 27127
 Description: Lemma for dfac11 27128. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.)
Hypotheses
Ref Expression
aomclem8.a
aomclem8.y
Assertion
Ref Expression
aomclem8
Distinct variable groups:   ,   ,,   ,,
Allowed substitution hints:   (,)   ()

Proof of Theorem aomclem8
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elequ2 1730 . . . . . . 7
2 elequ2 1730 . . . . . . . 8
32notbid 286 . . . . . . 7
41, 3bi2anan9r 845 . . . . . 6
5 elequ2 1730 . . . . . . . . 9
6 elequ2 1730 . . . . . . . . 9
75, 6bi2bian9 846 . . . . . . . 8
87imbi2d 308 . . . . . . 7
98ralbidv 2717 . . . . . 6
104, 9anbi12d 692 . . . . 5
1110rexbidv 2718 . . . 4
12 elequ1 1728 . . . . . . 7
13 elequ1 1728 . . . . . . . 8
1413notbid 286 . . . . . . 7
1512, 14anbi12d 692 . . . . . 6
16 breq2 4208 . . . . . . . . 9
1716imbi1d 309 . . . . . . . 8
1817ralbidv 2717 . . . . . . 7
19 breq1 4207 . . . . . . . . 9
20 elequ1 1728 . . . . . . . . . 10
21 elequ1 1728 . . . . . . . . . 10
2220, 21bibi12d 313 . . . . . . . . 9
2319, 22imbi12d 312 . . . . . . . 8
2423cbvralv 2924 . . . . . . 7
2518, 24syl6bb 253 . . . . . 6
2615, 25anbi12d 692 . . . . 5
2726cbvrexv 2925 . . . 4
2811, 27syl6bb 253 . . 3
2928cbvopabv 4269 . 2
30 nfcv 2571 . . 3
31 nfcv 2571 . . . 4
32 nfcv 2571 . . . 4
33 nfopab1 4266 . . . 4
3431, 32, 33nfsup 7448 . . 3
35 fveq2 5720 . . . 4
3635supeq1d 7443 . . 3
3730, 34, 36cbvmpt 4291 . 2
38 nfcv 2571 . . . 4
39 nffvmpt1 5728 . . . 4
40 rneq 5087 . . . . . 6
4140difeq2d 3457 . . . . 5
4241fveq2d 5724 . . . 4
4338, 39, 42cbvmpt 4291 . . 3
44 recseq 6626 . . 3 recs recs
4543, 44ax-mp 8 . 2 recs recs
46 nfv 1629 . . 3 recs recs
47 nfv 1629 . . 3 recs recs
48 nfmpt1 4290 . . . . . . . 8
4948nfrecs 6627 . . . . . . 7 recs
5049nfcnv 5043 . . . . . 6 recs
51 nfcv 2571 . . . . . 6
5250, 51nfima 5203 . . . . 5 recs
5352nfint 4052 . . . 4 recs
54 nfcv 2571 . . . . . 6
5550, 54nfima 5203 . . . . 5 recs
5655nfint 4052 . . . 4 recs
5753, 56nfel 2579 . . 3 recs recs
58 nfcv 2571 . . . . . . . . 9
59 nfcv 2571 . . . . . . . . . . . 12
60 nfcv 2571 . . . . . . . . . . . 12
61 nfopab2 4267 . . . . . . . . . . . 12
6259, 60, 61nfsup 7448 . . . . . . . . . . 11
6358, 62nfmpt 4289 . . . . . . . . . 10
64 nfcv 2571 . . . . . . . . . 10
6563, 64nffv 5727 . . . . . . . . 9
6658, 65nfmpt 4289 . . . . . . . 8
6766nfrecs 6627 . . . . . . 7 recs
6867nfcnv 5043 . . . . . 6 recs
69 nfcv 2571 . . . . . 6
7068, 69nfima 5203 . . . . 5 recs
7170nfint 4052 . . . 4 recs
72 nfcv 2571 . . . . . 6
7368, 72nfima 5203 . . . . 5 recs
7473nfint 4052 . . . 4 recs
7571, 74nfel 2579 . . 3 recs recs
76 sneq 3817 . . . . . 6
7776imaeq2d 5195 . . . . 5 recs recs
7877inteqd 4047 . . . 4 recs recs
79 sneq 3817 . . . . . 6
8079imaeq2d 5195 . . . . 5 recs recs
8180inteqd 4047 . . . 4 recs recs
82 eleq12 2497 . . . 4 recs recs recs recs recs recs recs recs
8378, 81, 82syl2an 464 . . 3 recs recs recs recs
8446, 47, 57, 75, 83cbvopab 4268 . 2 recs recs recs recs
85 fveq2 5720 . . . . 5
86 fveq2 5720 . . . . 5
8785, 86breqan12d 4219 . . . 4
8885, 86eqeqan12d 2450 . . . . 5
89 simpl 444 . . . . . 6
90 suceq 4638 . . . . . . . . 9
9185, 90syl 16 . . . . . . . 8
9291adantr 452 . . . . . . 7
9392fveq2d 5724 . . . . . 6
94 simpr 448 . . . . . 6
9589, 93, 94breq123d 4218 . . . . 5
9688, 95anbi12d 692 . . . 4
9787, 96orbi12d 691 . . 3
9897cbvopabv 4269 . 2
99 eqid 2435 . 2 recs recs recs recs
100 dmeq 5062 . . . . . . 7
101100unieqd 4018 . . . . . . 7
102100, 101eqeq12d 2449 . . . . . 6
103 fveq1 5719 . . . . . . . . . 10
104103breqd 4215 . . . . . . . . 9
105104anbi2d 685 . . . . . . . 8
106105orbi2d 683 . . . . . . 7
107106opabbidv 4263 . . . . . 6
108 eqidd 2436 . . . . . . . . . . . . . . . 16
109100fveq2d 5724 . . . . . . . . . . . . . . . 16
110101fveq2d 5724 . . . . . . . . . . . . . . . . . 18
111 id 20 . . . . . . . . . . . . . . . . . . . . . . 23
112111, 101fveq12d 5726 . . . . . . . . . . . . . . . . . . . . . 22
113112breqd 4215 . . . . . . . . . . . . . . . . . . . . 21
114113imbi1d 309 . . . . . . . . . . . . . . . . . . . 20
115110, 114raleqbidv 2908 . . . . . . . . . . . . . . . . . . 19
116115anbi2d 685 . . . . . . . . . . . . . . . . . 18
117110, 116rexeqbidv 2909 . . . . . . . . . . . . . . . . 17
118117opabbidv 4263 . . . . . . . . . . . . . . . 16
119108, 109, 118supeq123d 7447 . . . . . . . . . . . . . . 15
120119mpteq2dv 4288 . . . . . . . . . . . . . 14
121109difeq1d 3456 . . . . . . . . . . . . . 14
122120, 121fveq12d 5726 . . . . . . . . . . . . 13
123122mpteq2dv 4288 . . . . . . . . . . . 12
124 recseq 6626 . . . . . . . . . . . 12 recs recs
125123, 124syl 16 . . . . . . . . . . 11 recs recs
126125cnveqd 5040 . . . . . . . . . 10 recs recs
127126imaeq1d 5194 . . . . . . . . 9 recs recs
128127inteqd 4047 . . . . . . . 8 recs recs
129126imaeq1d 5194 . . . . . . . . 9 recs recs
130129inteqd 4047 . . . . . . . 8 recs recs
131128, 130eleq12d 2503 . . . . . . 7 recs recs recs recs
132131opabbidv 4263 . . . . . 6 recs recs recs recs
133102, 107, 132ifbieq12d 3753 . . . . 5 recs recs recs recs
134109, 109xpeq12d 4895 . . . . 5
135133, 134ineq12d 3535 . . . 4 recs recs recs recs
136135cbvmptv 4292 . . 3 recs recs recs recs
137 recseq 6626 . . 3 recs recs