MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axdc4lem Unicode version

Theorem axdc4lem 8856
Description: Lemma for axdc4 8857. (Contributed by Mario Carneiro, 31-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)
Hypotheses
Ref Expression
axdc4lem.1
axdc4lem.2
Assertion
Ref Expression
axdc4lem
Distinct variable groups:   , , , ,   , ,   , , ,   ,

Proof of Theorem axdc4lem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano1 6719 . . . 4
2 opelxpi 5036 . . . 4
31, 2mpan 670 . . 3
4 simp2 997 . . . . . . . 8
5 fovrn 6445 . . . . . . . 8
6 peano2 6720 . . . . . . . . . . 11
76snssd 4175 . . . . . . . . . 10
8 eldifi 3625 . . . . . . . . . 10
9 axdc4lem.1 . . . . . . . . . . . 12
109elpw2 4616 . . . . . . . . . . 11
11 xpss12 5113 . . . . . . . . . . 11
1210, 11sylan2b 475 . . . . . . . . . 10
137, 8, 12syl2an 477 . . . . . . . . 9
14 snex 4693 . . . . . . . . . . 11
15 ovex 6324 . . . . . . . . . . 11
1614, 15xpex 6604 . . . . . . . . . 10
1716elpw 4018 . . . . . . . . 9
1813, 17sylibr 212 . . . . . . . 8
194, 5, 18syl2anc 661 . . . . . . 7
20 eldifn 3626 . . . . . . . 8
2115elsnc 4053 . . . . . . . . . . 11
2221necon3bbii 2718 . . . . . . . . . 10
23 vex 3112 . . . . . . . . . . . . 13
2423sucex 6646 . . . . . . . . . . . 12
2524snnz 4148 . . . . . . . . . . 11
26 xpnz 5431 . . . . . . . . . . . 12
2726biimpi 194 . . . . . . . . . . 11
2825, 27mpan 670 . . . . . . . . . 10
2922, 28sylbi 195 . . . . . . . . 9
3016elsnc 4053 . . . . . . . . . 10
3130necon3bbii 2718 . . . . . . . . 9
3229, 31sylibr 212 . . . . . . . 8
335, 20, 323syl 20 . . . . . . 7
3419, 33eldifd 3486 . . . . . 6
35343expib 1199 . . . . 5
3635ralrimivv 2877 . . . 4
37 axdc4lem.2 . . . . 5
3837fmpt2 6867 . . . 4
3936, 38sylib 196 . . 3
40 dcomex 8848 . . . . 5
4140, 9xpex 6604 . . . 4
4241axdc3 8855 . . 3
433, 39, 42syl2an 477 . 2
44 2ndcof 6829 . . . . . . . . 9
45443ad2ant1 1017 . . . . . . . 8
4645adantl 466 . . . . . . 7
47 fex2 6755 . . . . . . . 8
4840, 9, 47mp3an23 1316 . . . . . . 7
4946, 48syl 16 . . . . . 6
50 fvco3 5950 . . . . . . . . . . 11
511, 50mpan2 671 . . . . . . . . . 10
52513ad2ant1 1017 . . . . . . . . 9
53 fveq2 5871 . . . . . . . . . 10
54533ad2ant2 1018 . . . . . . . . 9
5552, 54eqtrd 2498 . . . . . . . 8
56 op2ndg 6813 . . . . . . . . 9
571, 56mpan 670 . . . . . . . 8
5855, 57sylan9eqr 2520 . . . . . . 7
59 nfv 1707 . . . . . . . . 9
60 nfv 1707 . . . . . . . . . 10
61 nfv 1707 . . . . . . . . . 10
62 nfra1 2838 . . . . . . . . . 10
6360, 61, 62nf3an 1930 . . . . . . . . 9
6459, 63nfan 1928 . . . . . . . 8
65 fveq2 5871 . . . . . . . . . . . . . . . . 17
66 opeq1 4217 . . . . . . . . . . . . . . . . 17
6765, 66eqeq12d 2479 . . . . . . . . . . . . . . . 16
6867exbidv 1714 . . . . . . . . . . . . . . 15
69 fveq2 5871 . . . . . . . . . . . . . . . . 17
70 opeq1 4217 . . . . . . . . . . . . . . . . 17
7169, 70eqeq12d 2479 . . . . . . . . . . . . . . . 16
7271exbidv 1714 . . . . . . . . . . . . . . 15
73 fveq2 5871 . . . . . . . . . . . . . . . . 17
74 opeq1 4217 . . . . . . . . . . . . . . . . 17
7573, 74eqeq12d 2479 . . . . . . . . . . . . . . . 16
7675exbidv 1714 . . . . . . . . . . . . . . 15
77 opeq2 4218 . . . . . . . . . . . . . . . . . . 19
7877eqeq2d 2471 . . . . . . . . . . . . . . . . . 18
7978spcegv 3195 . . . . . . . . . . . . . . . . 17
8079imp 429 . . . . . . . . . . . . . . . 16
81803ad2antr2 1162 . . . . . . . . . . . . . . 15
82 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
83 df-ov 6299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8482, 83syl6eqr 2516 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8584adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
86 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . 26
87 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
88 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89 opelxp2 5038 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9088, 89syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9187, 90mpan9 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26
92 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9392sneqd 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9593, 94xpeq12d 5029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
96 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9796xpeq2d 5028 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
98 snex 4693 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99 ovex 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10098, 99xpex 6604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
10195, 97, 37, 100ovmpt2 6438 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10286, 91, 101syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25
10385, 102eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . 24
104 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105104fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
106 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
107106fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
108105, 107eleq12d 2539 . . . . . . . . . . . . . . . . . . . . . . . . . 26
109108rspcv 3206 . . . . . . . . . . . . . . . . . . . . . . . . 25
110109ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 24
111 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . 25
112 elxp 5021 . . . . . . . . . . . . . . . . . . . . . . . . . 26
113 elsn 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
114 opeq1 4217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
115113, 114sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
116115eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
117116biimpac 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
118117adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
119118eximi 1656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
120119exlimiv 1722 . . . . . . . . . . . . . . . . . . . . . . . . . 26
121112, 120sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . 25
122111, 121syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . 24
123103, 110, 122sylsyld 56 . . . . . . . . . . . . . . . . . . . . . . 23
124123expcom 435 . . . . . . . . . . . . . . . . . . . . . 22
125124exlimiv 1722 . . . . . . . . . . . . . . . . . . . . 21
126125com3l 81 . . . . . . . . . . . . . . . . . . . 20
127 opeq2 4218 . . . . . . . . . . . . . . . . . . . . . 22
128127eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . 21
129128cbvexv 2024 . . . . . . . . . . . . . . . . . . . 20
130126, 129syl8ib 231 . . . . . . . . . . . . . . . . . . 19
131130impancom 440 . . . . . . . . . . . . . . . . . 18
1321313adant2 1015 . . . . . . . . . . . . . . . . 17
133132adantl 466 . . . . . . . . . . . . . . . 16
134133com12 31 . . . . . . . . . . . . . . 15
13568, 72, 76, 81, 134finds2 6728 . . . . . . . . . . . . . 14
136135com12 31 . . . . . . . . . . . . 13
137136ralrimiv 2869 . . . . . . . . . . . 12
138 fveq2 5871 . . . . . . . . . . . . . . 15
139 opeq1 4217 . . . . . . . . . . . . . . 15
140138, 139eqeq12d 2479 . . . . . . . . . . . . . 14
141140exbidv 1714 . . . . . . . . . . . . 13
142141rspccv 3207 . . . . . . . . . . . 12
143137, 142syl 16 . . . . . . . . . . 11
1441433impia 1193 . . . . . . . . . 10
145 simp21 1029 . . . . . . . . . 10
146 simp3 998 . . . . . . . . . 10
147 rspa 2824 . . . . . . . . . . . 12
1481473ad2antl3 1160 . . . . . . . . . . 11
1491483adant1 1014 . . . . . . . . . 10
150 simpl 457 . . . . . . . . . . . . . . . . 17
151150fveq2d 5875 . . . . . . . . . . . . . . . 16
152 simprr 757 . . . . . . . . . . . . . . . . 17
153 ffvelrn 6029 . . . . . . . . . . . . . . . . . . 19
154 eleq1 2529 . . . . . . . . . . . . . . . . . . . 20
155 opelxp2 5038 . . . . . . . . . . . . . . . . . . . 20
156154, 155syl6bi 228 . . . . . . . . . . . . . . . . . . 19
157153, 156syl5 32 . . . . . . . . . . . . . . . . . 18
158157imp 429 . . . . . . . . . . . . . . . . 17
159 df-ov 6299 . . . . . . . . . . . . . . . . . 18
160 suceq 4948 . . . . . . . . . . . . . . . . . . . . 21
161160sneqd 4041 . . . . . . . . . . . . . . . . . . . 20
162 oveq1 6303 . . . . . . . . . . . . . . . . . . . 20
163161, 162xpeq12d 5029 . . . . . . . . . . . . . . . . . . 19
164 oveq2 6304 . . . . . . . . . . . . . . . . . . . 20
165164xpeq2d 5028 . . . . . . . . . . . . . . . . . . 19
166 snex 4693 . . . . . . . . . . . . . . . . . . . 20
167 ovex 6324 . . . . . . . . . . . . . . . . . . . 20
168166, 167xpex 6604 . . . . . . . . . . . . . . . . . . 19
169163, 165, 37, 168ovmpt2 6438 . . . . . . . . . . . . . . . . . 18
170159, 169syl5eqr 2512 . . . . . . . . . . . . . . . . 17
171152, 158, 170syl2anc 661 . . . . . . . . . . . . . . . 16
172151, 171eqtrd 2498 . . . . . . . . . . . . . . 15
173172eleq2d 2527 . . . . . . . . . . . . . 14
174 elxp 5021 . . . . . . . . . . . . . . . . 17
175 peano2 6720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
176 fvco3 5950 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
177175, 176sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26
178177adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
179 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . 26
180179fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . 25
181178, 180eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . 24
182 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . 25
183 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . 25
184182, 183op2nd 6809 . . . . . . . . . . . . . . . . . . . . . . . 24
185181, 184syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . 23
186 fvco3 5950 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
187186adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
188 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
189188fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . . 26
190187, 189eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . 25
191 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . 26
192 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . 26
193191, 192op2nd 6809 . . . . . . . . . . . . . . . . . . . . . . . . 25
194190, 193syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . . 24
195194oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . 23
196185, 195eleq12d 2539 . . . . . . . . . . . . . . . . . . . . . 22
197196biimprcd 225 . . . . . . . . . . . . . . . . . . . . 21