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

Theorem aomclem8 27159
 Description: Lemma for dfac11 27160. 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 1689 . . . . . . 7
2 elequ2 1689 . . . . . . . 8
32notbid 285 . . . . . . 7
41, 3bi2anan9r 844 . . . . . 6
5 elequ2 1689 . . . . . . . . 9
6 elequ2 1689 . . . . . . . . 9
75, 6bi2bian9 845 . . . . . . . 8
87imbi2d 307 . . . . . . 7
98ralbidv 2563 . . . . . 6
104, 9anbi12d 691 . . . . 5
1110rexbidv 2564 . . . 4
12 elequ1 1687 . . . . . . 7
13 elequ1 1687 . . . . . . . 8
1413notbid 285 . . . . . . 7
1512, 14anbi12d 691 . . . . . 6
16 breq2 4027 . . . . . . . . 9
1716imbi1d 308 . . . . . . . 8
1817ralbidv 2563 . . . . . . 7
19 breq1 4026 . . . . . . . . 9
20 elequ1 1687 . . . . . . . . . 10
21 elequ1 1687 . . . . . . . . . 10
2220, 21bibi12d 312 . . . . . . . . 9
2319, 22imbi12d 311 . . . . . . . 8
2423cbvralv 2764 . . . . . . 7
2518, 24syl6bb 252 . . . . . 6
2615, 25anbi12d 691 . . . . 5
2726cbvrexv 2765 . . . 4
2811, 27syl6bb 252 . . 3
2928cbvopabv 4088 . 2
30 nfcv 2419 . . 3
31 nfcv 2419 . . . 4
32 nfcv 2419 . . . 4
33 nfopab1 4085 . . . 4
3431, 32, 33nfsup 7202 . . 3
35 fveq2 5525 . . . 4
3635supeq1d 7199 . . 3
3730, 34, 36cbvmpt 4110 . 2
38 nfcv 2419 . . . 4
39 nfmpt1 4109 . . . . 5
40 nfcv 2419 . . . . 5
4139, 40nffv 5532 . . . 4
42 rneq 4904 . . . . . 6
4342difeq2d 3294 . . . . 5
4443fveq2d 5529 . . . 4
4538, 41, 44cbvmpt 4110 . . 3
46 recseq 6389 . . 3 recs recs
4745, 46ax-mp 8 . 2 recs recs
48 nfv 1605 . . 3 recs recs
49 nfv 1605 . . 3 recs recs
50 nfmpt1 4109 . . . . . . . 8
5150nfrecs 6390 . . . . . . 7 recs
5251nfcnv 4860 . . . . . 6 recs
53 nfcv 2419 . . . . . 6
5452, 53nfima 5020 . . . . 5 recs
5554nfint 3872 . . . 4 recs
56 nfcv 2419 . . . . . 6
5752, 56nfima 5020 . . . . 5 recs
5857nfint 3872 . . . 4 recs
5955, 58nfel 2427 . . 3 recs recs
60 nfcv 2419 . . . . . . . . 9
61 nfcv 2419 . . . . . . . . . . . 12
62 nfcv 2419 . . . . . . . . . . . 12
63 nfopab2 4086 . . . . . . . . . . . 12
6461, 62, 63nfsup 7202 . . . . . . . . . . 11
6560, 64nfmpt 4108 . . . . . . . . . 10
66 nfcv 2419 . . . . . . . . . 10
6765, 66nffv 5532 . . . . . . . . 9
6860, 67nfmpt 4108 . . . . . . . 8
6968nfrecs 6390 . . . . . . 7 recs
7069nfcnv 4860 . . . . . 6 recs
71 nfcv 2419 . . . . . 6
7270, 71nfima 5020 . . . . 5 recs
7372nfint 3872 . . . 4 recs
74 nfcv 2419 . . . . . 6
7570, 74nfima 5020 . . . . 5 recs
7675nfint 3872 . . . 4 recs
7773, 76nfel 2427 . . 3 recs recs
78 sneq 3651 . . . . . 6
7978imaeq2d 5012 . . . . 5 recs recs
8079inteqd 3867 . . . 4 recs recs
81 sneq 3651 . . . . . 6
8281imaeq2d 5012 . . . . 5 recs recs
8382inteqd 3867 . . . 4 recs recs
84 eleq12 2345 . . . 4 recs recs recs recs recs recs recs recs
8580, 83, 84syl2an 463 . . 3 recs recs recs recs
8648, 49, 59, 77, 85cbvopab 4087 . 2 recs recs recs recs
87 fveq2 5525 . . . . 5
88 fveq2 5525 . . . . 5
8987, 88breqan12d 4038 . . . 4
9087, 88eqeqan12d 2298 . . . . 5
91 simpl 443 . . . . . 6
92 suceq 4457 . . . . . . . . 9
9387, 92syl 15 . . . . . . . 8
9493adantr 451 . . . . . . 7
9594fveq2d 5529 . . . . . 6
96 simpr 447 . . . . . 6
9791, 95, 96breq123d 4037 . . . . 5
9890, 97anbi12d 691 . . . 4
9989, 98orbi12d 690 . . 3
10099cbvopabv 4088 . 2
101 eqid 2283 . 2 recs recs recs recs
102 dmeq 4879 . . . . . . 7
103102unieqd 3838 . . . . . . 7
104102, 103eqeq12d 2297 . . . . . 6
105 fveq1 5524 . . . . . . . . . 10
106105breqd 4034 . . . . . . . . 9
107106anbi2d 684 . . . . . . . 8
108107orbi2d 682 . . . . . . 7
109108opabbidv 4082 . . . . . 6
110 eqidd 2284 . . . . . . . . . . . . . . . 16
111102fveq2d 5529 . . . . . . . . . . . . . . . 16
112103fveq2d 5529 . . . . . . . . . . . . . . . . . 18
113 id 19 . . . . . . . . . . . . . . . . . . . . . . 23
114113, 103fveq12d 5531 . . . . . . . . . . . . . . . . . . . . . 22
115114breqd 4034 . . . . . . . . . . . . . . . . . . . . 21
116115imbi1d 308 . . . . . . . . . . . . . . . . . . . 20
117112, 116raleqbidv 2748 . . . . . . . . . . . . . . . . . . 19
118117anbi2d 684 . . . . . . . . . . . . . . . . . 18
119112, 118rexeqbidv 2749 . . . . . . . . . . . . . . . . 17
120119opabbidv 4082 . . . . . . . . . . . . . . . 16
121110, 111, 120supeq123d 27158 . . . . . . . . . . . . . . 15
122121mpteq2dv 4107 . . . . . . . . . . . . . 14
123111difeq1d 3293 . . . . . . . . . . . . . 14
124122, 123fveq12d 5531 . . . . . . . . . . . . 13
125124mpteq2dv 4107 . . . . . . . . . . . 12
126 recseq 6389 . . . . . . . . . . . 12 recs recs
127125, 126syl 15 . . . . . . . . . . 11 recs recs
128127cnveqd 4857 . . . . . . . . . 10 recs recs
129128imaeq1d 5011 . . . . . . . . 9 recs recs
130129inteqd 3867 . . . . . . . 8 recs recs
131128imaeq1d 5011 . . . . . . . . 9 recs recs
132131inteqd 3867 . . . . . . . 8 recs recs
133130, 132eleq12d 2351 . . . . . . 7 recs recs recs recs
134133opabbidv 4082 . . . . . 6 recs recs recs recs
135104, 109, 134ifbieq12d 3587 . . . . 5 recs recs recs recs
136111, 111xpeq12d 4714 . . . . 5
137135, 136ineq12d 3371 . . . 4 recs recs recs recs
138137cbvmptv 4111 . . 3 recs recs recs recs
139 recseq 6389 . . 3 recs