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

Theorem axdc3lem2 8834
 Description: Lemma for axdc3 8837. We have constructed a "candidate set" , which consists of all finite sequences that satisfy our property of interest, namely on its domain, but with the added constraint that . These sets are possible "initial segments" of the infinite sequence satisfying these constraints, but we can leverage the standard ax-dc 8829 (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely (for some integer ). We let our "choice" function select a sequence whose domain is one more than the last one, and agrees with the previous one on its domain. Thus, the application of vanilla ax-dc 8829 yields a sequence of sequences whose domains increase without bound, and whose union is a function which has all the properties we want. In this lemma, we show that given the sequence , we can construct the sequence that we are after. (Contributed by Mario Carneiro, 30-Jan-2013.)
Hypotheses
Ref Expression
axdc3lem2.1
axdc3lem2.2
axdc3lem2.3
Assertion
Ref Expression
axdc3lem2
Distinct variable groups:   ,,   ,,   ,,,   ,,,   ,,   ,,   ,   ,,   ,,   ,   ,,
Allowed substitution hints:   (,,)   (,)   (,,)   (,,)   (,,,,,)

Proof of Theorem axdc3lem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . . . . . . . . . 13
2 fveq2 5856 . . . . . . . . . . . . . 14
32dmeqd 5195 . . . . . . . . . . . . 13
41, 3eleq12d 2525 . . . . . . . . . . . 12
5 eleq2 2516 . . . . . . . . . . . . 13
62sseq2d 3517 . . . . . . . . . . . . 13
75, 6imbi12d 320 . . . . . . . . . . . 12
84, 7anbi12d 710 . . . . . . . . . . 11
9 id 22 . . . . . . . . . . . . 13
10 fveq2 5856 . . . . . . . . . . . . . 14
1110dmeqd 5195 . . . . . . . . . . . . 13
129, 11eleq12d 2525 . . . . . . . . . . . 12
13 elequ2 1809 . . . . . . . . . . . . 13
1410sseq2d 3517 . . . . . . . . . . . . 13
1513, 14imbi12d 320 . . . . . . . . . . . 12
1612, 15anbi12d 710 . . . . . . . . . . 11
17 id 22 . . . . . . . . . . . . 13
18 fveq2 5856 . . . . . . . . . . . . . 14
1918dmeqd 5195 . . . . . . . . . . . . 13
2017, 19eleq12d 2525 . . . . . . . . . . . 12
21 eleq2 2516 . . . . . . . . . . . . 13
2218sseq2d 3517 . . . . . . . . . . . . 13
2321, 22imbi12d 320 . . . . . . . . . . . 12
2420, 23anbi12d 710 . . . . . . . . . . 11
25 peano1 6704 . . . . . . . . . . . . . . 15
26 ffvelrn 6014 . . . . . . . . . . . . . . 15
2725, 26mpan2 671 . . . . . . . . . . . . . 14
28 axdc3lem2.2 . . . . . . . . . . . . . . . . . 18
29 fdm 5725 . . . . . . . . . . . . . . . . . . . . . . 23
30 nnord 6693 . . . . . . . . . . . . . . . . . . . . . . . . 25
31 0elsuc 6655 . . . . . . . . . . . . . . . . . . . . . . . . 25
3230, 31syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
33 peano2 6705 . . . . . . . . . . . . . . . . . . . . . . . 24
34 eleq2 2516 . . . . . . . . . . . . . . . . . . . . . . . . . 26
35 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3634, 35anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . 25
3736biimprcd 225 . . . . . . . . . . . . . . . . . . . . . . . 24
3832, 33, 37syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
3929, 38syl5com 30 . . . . . . . . . . . . . . . . . . . . . 22
40393ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . 21
4140impcom 430 . . . . . . . . . . . . . . . . . . . 20
4241rexlimiva 2931 . . . . . . . . . . . . . . . . . . 19
4342ss2abi 3557 . . . . . . . . . . . . . . . . . 18
4428, 43eqsstri 3519 . . . . . . . . . . . . . . . . 17
4544sseli 3485 . . . . . . . . . . . . . . . 16
46 fvex 5866 . . . . . . . . . . . . . . . . 17
47 dmeq 5193 . . . . . . . . . . . . . . . . . . 19
4847eleq2d 2513 . . . . . . . . . . . . . . . . . 18
4947eleq1d 2512 . . . . . . . . . . . . . . . . . 18
5048, 49anbi12d 710 . . . . . . . . . . . . . . . . 17
5146, 50elab 3232 . . . . . . . . . . . . . . . 16
5245, 51sylib 196 . . . . . . . . . . . . . . 15
5352simpld 459 . . . . . . . . . . . . . 14
5427, 53syl 16 . . . . . . . . . . . . 13
55 noel 3774 . . . . . . . . . . . . . 14
5655pm2.21i 131 . . . . . . . . . . . . 13
5754, 56jctir 538 . . . . . . . . . . . 12
5857adantr 465 . . . . . . . . . . 11
59 ffvelrn 6014 . . . . . . . . . . . . . . 15
6059ancoms 453 . . . . . . . . . . . . . 14
6160adantrr 716 . . . . . . . . . . . . 13
62 suceq 4933 . . . . . . . . . . . . . . . . 17
6362fveq2d 5860 . . . . . . . . . . . . . . . 16
64 fveq2 5856 . . . . . . . . . . . . . . . . 17
6564fveq2d 5860 . . . . . . . . . . . . . . . 16
6663, 65eleq12d 2525 . . . . . . . . . . . . . . 15
6766rspcva 3194 . . . . . . . . . . . . . 14
6867adantrl 715 . . . . . . . . . . . . 13
6944sseli 3485 . . . . . . . . . . . . . . . . . . . 20
70 fvex 5866 . . . . . . . . . . . . . . . . . . . . 21
71 dmeq 5193 . . . . . . . . . . . . . . . . . . . . . . 23
7271eleq2d 2513 . . . . . . . . . . . . . . . . . . . . . 22
7371eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22
7472, 73anbi12d 710 . . . . . . . . . . . . . . . . . . . . 21
7570, 74elab 3232 . . . . . . . . . . . . . . . . . . . 20
7669, 75sylib 196 . . . . . . . . . . . . . . . . . . 19
7776simprd 463 . . . . . . . . . . . . . . . . . 18
78 nnord 6693 . . . . . . . . . . . . . . . . . 18
79 ordsucelsuc 6642 . . . . . . . . . . . . . . . . . 18
8077, 78, 793syl 20 . . . . . . . . . . . . . . . . 17
8180adantr 465 . . . . . . . . . . . . . . . 16
82 dmeq 5193 . . . . . . . . . . . . . . . . . . . . . . . . . 26
83 suceq 4933 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8482, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
8584eqeq2d 2457 . . . . . . . . . . . . . . . . . . . . . . . 24
8682reseq2d 5263 . . . . . . . . . . . . . . . . . . . . . . . . 25
87 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25
8886, 87eqeq12d 2465 . . . . . . . . . . . . . . . . . . . . . . . 24
8985, 88anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . 23
9089rabbidv 3087 . . . . . . . . . . . . . . . . . . . . . 22
91 axdc3lem2.3 . . . . . . . . . . . . . . . . . . . . . 22
92 axdc3lem2.1 . . . . . . . . . . . . . . . . . . . . . . . 24
9392, 28axdc3lem 8833 . . . . . . . . . . . . . . . . . . . . . . 23
9493rabex 4588 . . . . . . . . . . . . . . . . . . . . . 22
9590, 91, 94fvmpt 5941 . . . . . . . . . . . . . . . . . . . . 21
9695eleq2d 2513 . . . . . . . . . . . . . . . . . . . 20
97 dmeq 5193 . . . . . . . . . . . . . . . . . . . . . . 23
9897eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . 22
99 reseq1 5257 . . . . . . . . . . . . . . . . . . . . . . 23
10099eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . 22
10198, 100anbi12d 710 . . . . . . . . . . . . . . . . . . . . 21
102101elrab 3243 . . . . . . . . . . . . . . . . . . . 20
10396, 102syl6bb 261 . . . . . . . . . . . . . . . . . . 19
104103simplbda 624 . . . . . . . . . . . . . . . . . 18
105104simpld 459 . . . . . . . . . . . . . . . . 17
106105eleq2d 2513 . . . . . . . . . . . . . . . 16
10781, 106bitr4d 256 . . . . . . . . . . . . . . 15
108107biimpd 207 . . . . . . . . . . . . . 14
109104simprd 463 . . . . . . . . . . . . . . 15
110 resss 5287 . . . . . . . . . . . . . . . 16
111 sseq1 3510 . . . . . . . . . . . . . . . 16
112110, 111mpbii 211 . . . . . . . . . . . . . . 15
113 elsuci 4934 . . . . . . . . . . . . . . . . 17
114 pm2.27 39 . . . . . . . . . . . . . . . . . . 19
115 sstr2 3496 . . . . . . . . . . . . . . . . . . 19
116114, 115syl6 33 . . . . . . . . . . . . . . . . . 18
117 fveq2 5856 . . . . . . . . . . . . . . . . . . . . 21
118117sseq1d 3516 . . . . . . . . . . . . . . . . . . . 20
119118biimprd 223 . . . . . . . . . . . . . . . . . . 19
120119a1d 25 . . . . . . . . . . . . . . . . . 18
121116, 120jaoi 379 . . . . . . . . . . . . . . . . 17
122113, 121syl 16 . . . . . . . . . . . . . . . 16
123122com13 80 . . . . . . . . . . . . . . 15
124109, 112, 1233syl 20 . . . . . . . . . . . . . 14
125108, 124anim12d 563 . . . . . . . . . . . . 13
12661, 68, 125syl2anc 661 . . . . . . . . . . . 12
127126ex 434 . . . . . . . . . . 11
1288, 16, 24, 58, 127finds2 6713 . . . . . . . . . 10
129128imp 429 . . . . . . . . 9
130129simprd 463 . . . . . . . 8
131130expcom 435 . . . . . . 7
132131ralrimdv 2859 . . . . . 6
133132ralrimiv 2855 . . . . 5
134 frn 5727 . . . . . . . . . . . 12
135 ffun 5723 . . . . . . . . . . . . . . . 16
1361353ad2ant1 1018 . . . . . . . . . . . . . . 15
137136rexlimivw 2932 . . . . . . . . . . . . . 14
138137ss2abi 3557 . . . . . . . . . . . . 13
13928, 138eqsstri 3519 . . . . . . . . . . . 12
140134, 139syl6ss 3501 . . . . . . . . . . 11
141140sseld 3488 . . . . . . . . . 10
142 vex 3098 . . . . . . . . . . 11
143 funeq 5597 . . . . . . . . . . 11
144142, 143elab 3232 . . . . . . . . . 10
145141, 144syl6ib 226 . . . . . . . . 9
146145adantr 465 . . . . . . . 8
147 ffn 5721 . . . . . . . . 9
148 fvelrnb 5905 . . . . . . . . . . . . 13
149 fvelrnb 5905 . . . . . . . . . . . . . . 15
150 nnord 6693 . . . . . . . . . . . . . . . . . . . . . . 23
151 nnord 6693 . . . . . . . . . . . . . . . . . . . . . . 23
152150, 151anim12i 566 . . . . . . . . . . . . . . . . . . . . . 22
153 ordtri3or 4900 . . . . . . . . . . . . . . . . . . . . . . 23
154 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
155154sseq2d 3517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
156155raleqbi1dv 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157156rspcv 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
158 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
159158sseq1d 3516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
160159rspccv 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161157, 160syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162161adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1631623imp 1191 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
164163orcd 392 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1651643exp 1196 . . . . . . . . . . . . . . . . . . . . . . . . 25
166165com3r 79 . . . . . . . . . . . . . . . . . . . . . . . 24
167 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
168 eqimss 3541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
169168orcd 392 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
170167, 169syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
171170a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . 25
172171a1d 25 . . . . . . . . . . . . . . . . . . . . . . . 24
173 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
174173sseq2d 3517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
175174raleqbi1dv 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
176175rspcv 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
177 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178177sseq1d 3516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179178rspccv 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180176, 179syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
181180adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1821813imp 1191 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
183182olcd 393 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1841833exp 1196 . . . . . . . . . . . . . . . . . . . . . . . . 25
185184com3r 79 . . . . . . . . . . . . . . . . . . . . . . . 24
186166, 172, 1853jaoi 1292 . . . . . . . . . . . . . . . . . . . . . . 23
187153, 186syl 16 . . . . . . . . . . . . . . . . . . . . . 22
188152, 187mpcom 36 . . . . . . . . . . . . . . . . . . . . 21
189 sseq12 3512 . . . . . . . . . . . . . . . . . . . . . . 23
190 sseq12 3512 . . . . . . . . . . . . . . . . . . . . . . . 24
191190ancoms 453 . . . . . . . . . . . . . . . . . . . . . . 23
192189, 191orbi12d 709 . . . . . . . . . . . . . . . . . . . . . 22
193192biimpcd 224 . . . . . . . . . . . . . . . . . . . . 21
194188, 193syl6 33 . . . . . . . . . . . . . . . . . . . 20
195194com23 78 . . . . . . . . . . . . . . . . . . 19
196195exp4b 607 . . . . . . . . . . . . . . . . . 18
197196com23 78 . . . . . . . . . . . . . . . . 17
198197rexlimiv 2929 . . . . . . . . . . . . . . . 16
199198rexlimdv 2933 . . . . . . . . . . . . . . 15
200149, 199syl6bi 228 . . . . . . . . . . . . . 14
201200com23 78 . . . . . . . . . . . . 13
202148, 201sylbid 215 . . . . . . . . . . . 12
203202com24 87 . . . . . . . . . . 11
204203imp 429 . . . . . . . . . 10
205204ralrimdv 2859 . . . . . . . . 9
206147, 205sylan 471 . . . . . . . 8
207146, 206jcad 533 . . . . . . 7
208207ralrimiv 2855 . . . . . 6
209 fununi 5644 . . . . . 6
210208, 209syl 16 . . . . 5
211133, 210syldan 470 . . . 4
212 vex 3098 . . . . . . . . 9
213212eldm2 5191 . . . . . . . 8
214 eluni2 4238 . . . . . . . . . 10
215212, 142opeldm 5196 . . . . . . . . . . . . . . 15
216215a1i 11 . . . . . . . . . . . . . 14
217134, 44syl6ss 3501 . . . . . . . . . . . . . . 15
218 ssel 3483 . . . . . . . . . . . . . . . 16
219 vex 3098 . . . . . . . . . . . . . . . . . 18
220 dmeq 5193 . . . . . . . . . . . . . . . . . . . 20
221220eleq2d 2513 . . . . . . . . . . . . . . . . . . 19
222220eleq1d 2512 . . . . . . . . . . . . . . . . . . 19
223221, 222anbi12d 710 . . . . . . . . . . . . . . . . . 18
224219, 223elab 3232 . . . . . . . . . . . . . . . . 17
225224simprbi 464 . . . . . . . . . . . . . . . 16
226218, 225syl6 33 . . . . . . . . . . . . . . 15
227217, 226syl 16 . . . . . . . . . . . . . 14
228216, 227anim12d 563 . . . . . . . . . . . . 13
229 elnn 6695 . . . . . . . . . . . . 13
230228, 229syl6 33 . . . . . . . . . . . 12
231230expcomd 438 . . . . . . . . . . 11
232231rexlimdv 2933 . . . . . . . . . 10
233214, 232syl5bi 217 . . . . . . . . 9
234233exlimdv 1711 . . . . . . . 8
235213, 234syl5bi 217 . . . . . . 7
236235adantr 465 . . . . . 6
237129simpld 459 . . . . . . . . 9
238 fnfvelrn 6013 . . . . . . . . . . . . 13
239 dmeq 5193 . . . . . . . . . . . . . . . 16
240239eleq2d 2513 . . . . . . . . . . . . . . 15
241240rspcev 3196 . . . . . . . . . . . . . 14
242241ex 434 . . . . . . . . . . . . 13
243238, 242syl 16 . . . . . . . . . . . 12
244147, 243sylan 471 . . . . . . . . . . 11
245244ancoms 453 . . . . . . . . . 10
246245adantrr 716 . . . . . . . . 9
247237, 246mpd 15 . . . . . . . 8
248 dmuni 5202 . . . . . . . . . 10
249248eleq2i 2521 . . . . . . . . 9
250 eliun 4320 . . . . . . . . 9
251249, 250bitri 249 . . . . . . . 8
252247, 251sylibr 212 . . . . . . 7
253252expcom 435 . . . . . 6
254236, 253impbid 191 . . . . 5
255254eqrdv 2440 . . . 4
256 rnuni 5407 . . . . . 6
257 frn 5727 . . . . . . . . . . . . . 14
2582573ad2ant1 1018 . . . . . . . . . . . . 13
259258rexlimivw 2932 . . . . . . . . . . . 12
260259ss2abi 3557 . . . . . . . . . . 11
26128, 260eqsstri 3519 . . . . . . . . . 10
262134, 261syl6ss 3501 . . . . . . . . 9
263 ssel 3483 . . . . . . . . . 10
264 abid 2430 . . . . . . . . . 10
265263, 264syl6ib 226 . . . . . . . . 9
266262, 265syl 16 . . . . . . . 8
267266ralrimiv 2855 . . . . . . 7
268 iunss 4356 . . . . . . 7
269267, 268sylibr 212 . . . . . 6
270256, 269syl5eqss 3533 . . . . 5
271270adantr 465 . . . 4
272 df-fn 5581 . . . . 5
273 df-f 5582 . . . . . 6
274273biimpri 206 . . . . 5
275272, 274sylanbr 473 . . . 4
276211, 255, 271, 275syl21anc 1228 . . 3
277 fnfvelrn 6013 . . . . . . . 8
278147, 25, 277sylancl 662 . . . . . . 7
279278adantr 465 . . . . . 6
280 elssuni 4264 . . . . . 6
281279, 280syl 16 . . . . 5
28254adantr 465 . . . . 5
283 funssfv 5871 . . . . 5
284211, 281, 282, 283syl3anc 1229 . . . 4
285 simp2 998 . . . . . . . . . . 11
286285rexlimivw 2932 . . . . . . . . . 10
287286ss2abi 3557 . . . . . . . . 9
28828, 287eqsstri 3519 . . . . . . . 8
289134, 288syl6ss 3501 . . . . . . 7
290 ssel 3483 . . . . . . . 8
291 fveq1 5855 . . . . . . . . . 10
292291eqeq1d 2445 . . . . . . . . 9
29346, 292elab 3232 . . . . . . . 8
294290, 293syl6ib 226 . . . . . . 7
295289, 294syl 16 . . . . . 6
296295adantr 465 . . . . 5
297279, 296mpd 15 . . . 4
298284, 297eqtrd 2484 . . 3
299 nfv 1694 . . . . 5
300 nfra1 2824 . . . . 5
301299, 300nfan 1914 . . . 4
302134ad2antrr 725 . . . . . . 7
303 peano2 6705 . . . . . . . . 9
304 fnfvelrn 6013 . . . . . . . . 9
305147, 303, 304syl2an 477 . . . . . . . 8
306305adantlr 714 . . . . . . 7
307237expcom 435 . . . . . . . . 9
308307ralrimiv 2855 . . . . . . . 8
309 id 22 . . . . . . . . . . 11
310 fveq2 5856 . . . . . . . . . . . 12
311310dmeqd 5195 . . . . . . . . . . 11
312309, 311eleq12d 2525 . . . . . . . . . 10
313312rspcv 3192 . . . . . . . . 9
314303, 313syl 16 . . . . . . . 8
315308, 314mpan9 469 . . . . . . 7
316 eleq2 2516 . . . . . . . . . . . . . . . . . . . . 21
317316biimpa 484 . . . . . . . . . . . . . . . . . . . 20
31829, 317sylan 471 . . . . . . . . . . . . . . . . . . 19
319 ordsucelsuc 6642 . . . . . . . . . . . . . . . . . . . . . . 23
32030, 319syl 16 . . . . . . . . . . . . . . . . . . . . . 22
321320biimprd 223 . . . . . . . . . . . . . . . . . . . . 21
322 rsp 2809 . . . . . . . . . . . . . . . . . . . . 21
323321, 322syl9r 72 . . . . . . . . . . . . . . . . . . . 20
324323com13 80 . . . . . . . . . . . . . . . . . . 19
325318, 324syl 16 . . . . . . . . . . . . . . . . . 18
326325ex 434 . . . . . . . . . . . . . . . . 17
327326com24 87 . . . . . . . . . . . . . . . 16
328327imp 429 . . . . . . . . . . . . . . 15
3293283adant2 1016 . . . . . . . . . . . . . 14
330329impcom 430 . . . . . . . . . . . . 13
331330rexlimiva 2931 . . . . . . . . . . . 12
332331ss2abi 3557 . . . . . . . . . . 11
33328, 332eqsstri 3519 . . . . . . . . . 10
334 sstr 3497 . . . . . . . . . 10
335333, 334mpan2 671 . . . . . . . . 9
336335sseld 3488 . . . . . . . 8
337 fvex 5866 . . . . . . . . 9
338 dmeq 5193 . . . . . . . . . . 11
339338eleq2d 2513 . . . . . . . . . 10
340 fveq1 5855 . . . . . . . . . . 11
341 fveq1 5855 . . . . . . . . . . . 12
342341fveq2d 5860 . . . . . . . . . . 11
343340, 342eleq12d 2525 . . . . . . . . . 10
344339, 343imbi12d 320 . . . . . . . . 9
345337, 344elab 3232 . . . . . . . 8
346336, 345syl6ib 226 . . . . . . 7
347302, 306, 315, 346syl3c 61 . . . . . 6
348211adantr 465 . . . . . . . 8
349 elssuni 4264 . . . . . . . . . 10
350305, 349syl 16 . . . . . . . . 9
351350adantlr 714 . . . . . . . 8
352 funssfv 5871 . . . . . . . 8
353348, 351, 315, 352syl3anc 1229 . . . . . . 7
354217sseld 3488 . . . . . . . . . . . . . . 15
355338eleq2d 2513 . . . . . . . . . . . . . . . . 17
356338eleq1d 2512 . . . . . . . . . . . . . . . . 17
357355, 356anbi12d 710 . . . . . . . . . . . . . . . 16
358337, 357elab 3232 . . . . . . . . . . . . . . 15
359354, 358syl6ib 226 . . . . . . . . . . . . . 14
360359adantr 465 . . . . . . . . . . . . 13
361305, 360mpd 15 . . . . . . . . . . . 12
362361simprd 463 . . . . . . . . . . 11
363 nnord 6693 . . . . . . . . . . 11
364 ordtr 4882 . . . . . . . . . . 11
365 trsuc 4952 . . . . . . . . . . . 12
366365ex 434 . . . . . . . . . . 11
367362, 363, 364, 3664syl 21 . . . . . . . . . 10
368367adantlr 714 . . . . . . . . 9
369315, 368mpd 15 . . . . . . . 8
370 funssfv 5871 . . . . . . . 8
371348, 351, 369, 370syl3anc 1229 . . . . . . 7
372 simpl 457 . . . . . . . 8
373 simpr 461 . . . . . . . . 9
374373fveq2d 5860 . . . . . . . 8
375372, 374eleq12d 2525 . . . . . . 7
376353, 371, 375syl2anc 661 . . . . . 6
377347, 376mpbird 232 . . . . 5
378377ex 434 . . . 4
379301, 378ralrimi 2843 . . 3
380 vex 3098 . . . . . 6
381380rnex 6719 . . . . 5
382381uniex 6581 . . . 4
383 feq1 5703 . . . . 5
384 fveq1 5855 . . . . . 6
385384eqeq1d 2445 . . . . 5
386 fveq1 5855 . . . . . . 7
387 fveq1 5855 . . . . . . . 8
388387fveq2d 5860 . . . . . . 7
389386, 388eleq12d 2525 . . . . . 6
390389ralbidv 2882 . . . . 5
391383, 385, 3903anbi123d 1300 . . . 4
392382, 391spcev 3187 . . 3
393276, 298, 379, 392syl3anc 1229 . 2
394393exlimiv 1709 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wo 368   wa 369   w3o 973   w3a 974   wceq 1383  wex 1599   wcel 1804  cab 2428  wral 2793  wrex 2794  crab 2797  cvv 3095   wss 3461  c0 3770  cop 4020  cuni 4234  ciun 4315   cmpt 4495   wtr 4530   word 4867   csuc 4870   cdm 4989   crn 4990   cres 4991   wfun 5572   wfn 5573  wf 5574  cfv 5578  com 6685 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-dc 8829 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586  df-om 6686  df-1o 7132 This theorem is referenced by:  axdc3lem4  8836
 Copyright terms: Public domain W3C validator