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

Theorem axdc3lem2 8323
 Description: Lemma for axdc3 8326. 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 8318 (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 8318 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 20 . . . . . . . . . . . . 13
2 fveq2 5720 . . . . . . . . . . . . . 14
32dmeqd 5064 . . . . . . . . . . . . 13
41, 3eleq12d 2503 . . . . . . . . . . . 12
5 eleq2 2496 . . . . . . . . . . . . 13
62sseq2d 3368 . . . . . . . . . . . . 13
75, 6imbi12d 312 . . . . . . . . . . . 12
84, 7anbi12d 692 . . . . . . . . . . 11
9 id 20 . . . . . . . . . . . . 13
10 fveq2 5720 . . . . . . . . . . . . . 14
1110dmeqd 5064 . . . . . . . . . . . . 13
129, 11eleq12d 2503 . . . . . . . . . . . 12
13 elequ2 1730 . . . . . . . . . . . . 13
1410sseq2d 3368 . . . . . . . . . . . . 13
1513, 14imbi12d 312 . . . . . . . . . . . 12
1612, 15anbi12d 692 . . . . . . . . . . 11
17 id 20 . . . . . . . . . . . . 13
18 fveq2 5720 . . . . . . . . . . . . . 14
1918dmeqd 5064 . . . . . . . . . . . . 13
2017, 19eleq12d 2503 . . . . . . . . . . . 12
21 eleq2 2496 . . . . . . . . . . . . 13
2218sseq2d 3368 . . . . . . . . . . . . 13
2321, 22imbi12d 312 . . . . . . . . . . . 12
2420, 23anbi12d 692 . . . . . . . . . . 11
25 peano1 4856 . . . . . . . . . . . . . . 15
26 ffvelrn 5860 . . . . . . . . . . . . . . 15
2725, 26mpan2 653 . . . . . . . . . . . . . 14
28 axdc3lem2.2 . . . . . . . . . . . . . . . . . 18
29 fdm 5587 . . . . . . . . . . . . . . . . . . . . . . 23
30 nnord 4845 . . . . . . . . . . . . . . . . . . . . . . . . 25
31 0elsuc 4807 . . . . . . . . . . . . . . . . . . . . . . . . 25
3230, 31syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
33 peano2 4857 . . . . . . . . . . . . . . . . . . . . . . . 24
34 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . . . . . 26
35 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3634, 35anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . 25
3736biimprcd 217 . . . . . . . . . . . . . . . . . . . . . . . 24
3832, 33, 37syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
3929, 38syl5com 28 . . . . . . . . . . . . . . . . . . . . . 22
40393ad2ant1 978 . . . . . . . . . . . . . . . . . . . . 21
4140impcom 420 . . . . . . . . . . . . . . . . . . . 20
4241rexlimiva 2817 . . . . . . . . . . . . . . . . . . 19
4342ss2abi 3407 . . . . . . . . . . . . . . . . . 18
4428, 43eqsstri 3370 . . . . . . . . . . . . . . . . 17
4544sseli 3336 . . . . . . . . . . . . . . . 16
46 fvex 5734 . . . . . . . . . . . . . . . . 17
47 dmeq 5062 . . . . . . . . . . . . . . . . . . 19
4847eleq2d 2502 . . . . . . . . . . . . . . . . . 18
4947eleq1d 2501 . . . . . . . . . . . . . . . . . 18
5048, 49anbi12d 692 . . . . . . . . . . . . . . . . 17
5146, 50elab 3074 . . . . . . . . . . . . . . . 16
5245, 51sylib 189 . . . . . . . . . . . . . . 15
5352simpld 446 . . . . . . . . . . . . . 14
5427, 53syl 16 . . . . . . . . . . . . 13
55 noel 3624 . . . . . . . . . . . . . 14
5655pm2.21i 125 . . . . . . . . . . . . 13
5754, 56jctir 525 . . . . . . . . . . . 12
5857adantr 452 . . . . . . . . . . 11
59 ffvelrn 5860 . . . . . . . . . . . . . . 15
6059ancoms 440 . . . . . . . . . . . . . 14
6160adantrr 698 . . . . . . . . . . . . 13
62 suceq 4638 . . . . . . . . . . . . . . . . 17
6362fveq2d 5724 . . . . . . . . . . . . . . . 16
64 fveq2 5720 . . . . . . . . . . . . . . . . 17
6564fveq2d 5724 . . . . . . . . . . . . . . . 16
6663, 65eleq12d 2503 . . . . . . . . . . . . . . 15
6766rspcva 3042 . . . . . . . . . . . . . 14
6867adantrl 697 . . . . . . . . . . . . 13
6944sseli 3336 . . . . . . . . . . . . . . . . . . . 20
70 fvex 5734 . . . . . . . . . . . . . . . . . . . . 21
71 dmeq 5062 . . . . . . . . . . . . . . . . . . . . . . 23
7271eleq2d 2502 . . . . . . . . . . . . . . . . . . . . . 22
7371eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . 22
7472, 73anbi12d 692 . . . . . . . . . . . . . . . . . . . . 21
7570, 74elab 3074 . . . . . . . . . . . . . . . . . . . 20
7669, 75sylib 189 . . . . . . . . . . . . . . . . . . 19
7776simprd 450 . . . . . . . . . . . . . . . . . 18
78 nnord 4845 . . . . . . . . . . . . . . . . . 18
79 ordsucelsuc 4794 . . . . . . . . . . . . . . . . . 18
8077, 78, 793syl 19 . . . . . . . . . . . . . . . . 17
8180adantr 452 . . . . . . . . . . . . . . . 16
82 dmeq 5062 . . . . . . . . . . . . . . . . . . . . . . . . . 26
83 suceq 4638 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8482, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
8584eqeq2d 2446 . . . . . . . . . . . . . . . . . . . . . . . 24
8682reseq2d 5138 . . . . . . . . . . . . . . . . . . . . . . . . 25
87 id 20 . . . . . . . . . . . . . . . . . . . . . . . . 25
8886, 87eqeq12d 2449 . . . . . . . . . . . . . . . . . . . . . . . 24
8985, 88anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . 23
9089rabbidv 2940 . . . . . . . . . . . . . . . . . . . . . 22
91 axdc3lem2.3 . . . . . . . . . . . . . . . . . . . . . 22
92 axdc3lem2.1 . . . . . . . . . . . . . . . . . . . . . . . 24
9392, 28axdc3lem 8322 . . . . . . . . . . . . . . . . . . . . . . 23
9493rabex 4346 . . . . . . . . . . . . . . . . . . . . . 22
9590, 91, 94fvmpt 5798 . . . . . . . . . . . . . . . . . . . . 21
9695eleq2d 2502 . . . . . . . . . . . . . . . . . . . 20
97 dmeq 5062 . . . . . . . . . . . . . . . . . . . . . . 23
9897eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . 22
99 reseq1 5132 . . . . . . . . . . . . . . . . . . . . . . 23
10099eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . 22
10198, 100anbi12d 692 . . . . . . . . . . . . . . . . . . . . 21
102101elrab 3084 . . . . . . . . . . . . . . . . . . . 20
10396, 102syl6bb 253 . . . . . . . . . . . . . . . . . . 19
104103simplbda 608 . . . . . . . . . . . . . . . . . 18
105104simpld 446 . . . . . . . . . . . . . . . . 17
106105eleq2d 2502 . . . . . . . . . . . . . . . 16
10781, 106bitr4d 248 . . . . . . . . . . . . . . 15
108107biimpd 199 . . . . . . . . . . . . . 14
109104simprd 450 . . . . . . . . . . . . . . 15
110 resss 5162 . . . . . . . . . . . . . . . 16
111 sseq1 3361 . . . . . . . . . . . . . . . 16
112110, 111mpbii 203 . . . . . . . . . . . . . . 15
113 elsuci 4639 . . . . . . . . . . . . . . . . 17
114 pm2.27 37 . . . . . . . . . . . . . . . . . . 19
115 sstr2 3347 . . . . . . . . . . . . . . . . . . 19
116114, 115syl6 31 . . . . . . . . . . . . . . . . . 18
117 fveq2 5720 . . . . . . . . . . . . . . . . . . . . 21
118117sseq1d 3367 . . . . . . . . . . . . . . . . . . . 20
119118biimprd 215 . . . . . . . . . . . . . . . . . . 19
120119a1d 23 . . . . . . . . . . . . . . . . . 18
121116, 120jaoi 369 . . . . . . . . . . . . . . . . 17
122113, 121syl 16 . . . . . . . . . . . . . . . 16
123122com13 76 . . . . . . . . . . . . . . 15
124109, 112, 1233syl 19 . . . . . . . . . . . . . 14
125108, 124anim12d 547 . . . . . . . . . . . . 13
12661, 68, 125syl2anc 643 . . . . . . . . . . . 12
127126ex 424 . . . . . . . . . . 11
1288, 16, 24, 58, 127finds2 4865 . . . . . . . . . 10
129128imp 419 . . . . . . . . 9
130129simprd 450 . . . . . . . 8
131130expcom 425 . . . . . . 7
132131ralrimdv 2787 . . . . . 6
133132ralrimiv 2780 . . . . 5
134 frn 5589 . . . . . . . . . . . 12
135 ffun 5585 . . . . . . . . . . . . . . . 16
1361353ad2ant1 978 . . . . . . . . . . . . . . 15
137136rexlimivw 2818 . . . . . . . . . . . . . 14
138137ss2abi 3407 . . . . . . . . . . . . 13
13928, 138eqsstri 3370 . . . . . . . . . . . 12
140134, 139syl6ss 3352 . . . . . . . . . . 11
141140sseld 3339 . . . . . . . . . 10
142 vex 2951 . . . . . . . . . . 11
143 funeq 5465 . . . . . . . . . . 11
144142, 143elab 3074 . . . . . . . . . 10
145141, 144syl6ib 218 . . . . . . . . 9
146145adantr 452 . . . . . . . 8
147 ffn 5583 . . . . . . . . 9
148 fvelrnb 5766 . . . . . . . . . . . . 13
149 fvelrnb 5766 . . . . . . . . . . . . . . 15
150 nnord 4845 . . . . . . . . . . . . . . . . . . . . . . 23
151 nnord 4845 . . . . . . . . . . . . . . . . . . . . . . 23
152150, 151anim12i 550 . . . . . . . . . . . . . . . . . . . . . 22
153 ordtri3or 4605 . . . . . . . . . . . . . . . . . . . . . . 23
154 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
155154sseq2d 3368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
156155raleqbi1dv 2904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157156rspcv 3040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
158 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
159158sseq1d 3367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
160159rspccv 3041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161157, 160syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162161adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1631623imp 1147 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
164163orcd 382 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1651643exp 1152 . . . . . . . . . . . . . . . . . . . . . . . . 25
166165com3r 75 . . . . . . . . . . . . . . . . . . . . . . . 24
167 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
168 eqimss 3392 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
169168orcd 382 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
170167, 169syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
171170a1d 23 . . . . . . . . . . . . . . . . . . . . . . . . 25
172171a1d 23 . . . . . . . . . . . . . . . . . . . . . . . 24
173 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
174173sseq2d 3368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
175174raleqbi1dv 2904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
176175rspcv 3040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
177 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178177sseq1d 3367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179178rspccv 3041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180176, 179syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
181180adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1821813imp 1147 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
183182olcd 383 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1841833exp 1152 . . . . . . . . . . . . . . . . . . . . . . . . 25
185184com3r 75 . . . . . . . . . . . . . . . . . . . . . . . 24
186166, 172, 1853jaoi 1247 . . . . . . . . . . . . . . . . . . . . . . 23
187153, 186syl 16 . . . . . . . . . . . . . . . . . . . . . 22
188152, 187mpcom 34 . . . . . . . . . . . . . . . . . . . . 21
189 sseq12 3363 . . . . . . . . . . . . . . . . . . . . . . 23
190 sseq12 3363 . . . . . . . . . . . . . . . . . . . . . . . 24
191190ancoms 440 . . . . . . . . . . . . . . . . . . . . . . 23
192189, 191orbi12d 691 . . . . . . . . . . . . . . . . . . . . . 22
193192biimpcd 216 . . . . . . . . . . . . . . . . . . . . 21
194188, 193syl6 31 . . . . . . . . . . . . . . . . . . . 20
195194com23 74 . . . . . . . . . . . . . . . . . . 19
196195exp4b 591 . . . . . . . . . . . . . . . . . 18
197196com23 74 . . . . . . . . . . . . . . . . 17
198197rexlimiv 2816 . . . . . . . . . . . . . . . 16
199198rexlimdv 2821 . . . . . . . . . . . . . . 15
200149, 199syl6bi 220 . . . . . . . . . . . . . 14
201200com23 74 . . . . . . . . . . . . 13
202148, 201sylbid 207 . . . . . . . . . . . 12
203202com24 83 . . . . . . . . . . 11
204203imp 419 . . . . . . . . . 10
205204ralrimdv 2787 . . . . . . . . 9
206147, 205sylan 458 . . . . . . . 8
207146, 206jcad 520 . . . . . . 7
208207ralrimiv 2780 . . . . . 6
209 fununi 5509 . . . . . 6
210208, 209syl 16 . . . . 5
211133, 210syldan 457 . . . 4
212 vex 2951 . . . . . . . . 9
213212eldm2 5060 . . . . . . . 8
214 eluni2 4011 . . . . . . . . . 10
215212, 142opeldm 5065 . . . . . . . . . . . . . . 15
216215a1i 11 . . . . . . . . . . . . . 14
217134, 44syl6ss 3352 . . . . . . . . . . . . . . 15
218 ssel 3334 . . . . . . . . . . . . . . . 16
219 vex 2951 . . . . . . . . . . . . . . . . . 18
220 dmeq 5062 . . . . . . . . . . . . . . . . . . . 20
221220eleq2d 2502 . . . . . . . . . . . . . . . . . . 19
222220eleq1d 2501 . . . . . . . . . . . . . . . . . . 19
223221, 222anbi12d 692 . . . . . . . . . . . . . . . . . 18
224219, 223elab 3074 . . . . . . . . . . . . . . . . 17
225224simprbi 451 . . . . . . . . . . . . . . . 16
226218, 225syl6 31 . . . . . . . . . . . . . . 15
227217, 226syl 16 . . . . . . . . . . . . . 14
228216, 227anim12d 547 . . . . . . . . . . . . 13
229 elnn 4847 . . . . . . . . . . . . 13
230228, 229syl6 31 . . . . . . . . . . . 12
231230exp3acom23 1381 . . . . . . . . . . 11
232231rexlimdv 2821 . . . . . . . . . 10
233214, 232syl5bi 209 . . . . . . . . 9
234233exlimdv 1646 . . . . . . . 8
235213, 234syl5bi 209 . . . . . . 7
236235adantr 452 . . . . . 6
237129simpld 446 . . . . . . . . 9
238 fnfvelrn 5859 . . . . . . . . . . . . 13
239 dmeq 5062 . . . . . . . . . . . . . . . 16
240239eleq2d 2502 . . . . . . . . . . . . . . 15
241240rspcev 3044 . . . . . . . . . . . . . 14
242241ex 424 . . . . . . . . . . . . 13
243238, 242syl 16 . . . . . . . . . . . 12
244147, 243sylan 458 . . . . . . . . . . 11
245244ancoms 440 . . . . . . . . . 10
246245adantrr 698 . . . . . . . . 9
247237, 246mpd 15 . . . . . . . 8
248 dmuni 5071 . . . . . . . . . 10
249248eleq2i 2499 . . . . . . . . 9
250 eliun 4089 . . . . . . . . 9
251249, 250bitri 241 . . . . . . . 8
252247, 251sylibr 204 . . . . . . 7
253252expcom 425 . . . . . 6
254236, 253impbid 184 . . . . 5
255254eqrdv 2433 . . . 4
256 rnuni 5275 . . . . . 6
257 frn 5589 . . . . . . . . . . . . . 14
2582573ad2ant1 978 . . . . . . . . . . . . 13
259258rexlimivw 2818 . . . . . . . . . . . 12
260259ss2abi 3407 . . . . . . . . . . 11
26128, 260eqsstri 3370 . . . . . . . . . 10
262134, 261syl6ss 3352 . . . . . . . . 9
263 ssel 3334 . . . . . . . . . 10
264 abid 2423 . . . . . . . . . 10
265263, 264syl6ib 218 . . . . . . . . 9
266262, 265syl 16 . . . . . . . 8
267266ralrimiv 2780 . . . . . . 7
268 iunss 4124 . . . . . . 7
269267, 268sylibr 204 . . . . . 6
270256, 269syl5eqss 3384 . . . . 5
271270adantr 452 . . . 4
272 df-fn 5449 . . . . 5
273 df-f 5450 . . . . . 6
274273biimpri 198 . . . . 5
275272, 274sylanbr 460 . . . 4
276211, 255, 271, 275syl21anc 1183 . . 3
277 fnfvelrn 5859 . . . . . . . 8
278147, 25, 277sylancl 644 . . . . . . 7
279278adantr 452 . . . . . 6
280 elssuni 4035 . . . . . 6
281279, 280syl 16 . . . . 5
28254adantr 452 . . . . 5
283 funssfv 5738 . . . . 5
284211, 281, 282, 283syl3anc 1184 . . . 4
285 simp2 958 . . . . . . . . . . 11
286285rexlimivw 2818 . . . . . . . . . 10
287286ss2abi 3407 . . . . . . . . 9
28828, 287eqsstri 3370 . . . . . . . 8
289134, 288syl6ss 3352 . . . . . . 7
290 ssel 3334 . . . . . . . 8
291 fveq1 5719 . . . . . . . . . 10
292291eqeq1d 2443 . . . . . . . . 9
29346, 292elab 3074 . . . . . . . 8
294290, 293syl6ib 218 . . . . . . 7
295289, 294syl 16 . . . . . 6
296295adantr 452 . . . . 5
297279, 296mpd 15 . . . 4
298284, 297eqtrd 2467 . . 3
299 nfv 1629 . . . . 5
300 nfra1 2748 . . . . 5
301299, 300nfan 1846 . . . 4
302134ad2antrr 707 . . . . . . 7
303 peano2 4857 . . . . . . . . 9
304 fnfvelrn 5859 . . . . . . . . 9
305147, 303, 304syl2an 464 . . . . . . . 8
306305adantlr 696 . . . . . . 7
307237expcom 425 . . . . . . . . 9
308307ralrimiv 2780 . . . . . . . 8
309 id 20 . . . . . . . . . . 11
310 fveq2 5720 . . . . . . . . . . . 12
311310dmeqd 5064 . . . . . . . . . . 11
312309, 311eleq12d 2503 . . . . . . . . . 10
313312rspcv 3040 . . . . . . . . 9
314303, 313syl 16 . . . . . . . 8
315308, 314mpan9 456 . . . . . . 7
316 eleq2 2496 . . . . . . . . . . . . . . . . . . . . 21
317316biimpa 471 . . . . . . . . . . . . . . . . . . . 20
31829, 317sylan 458 . . . . . . . . . . . . . . . . . . 19
319 ordsucelsuc 4794 . . . . . . . . . . . . . . . . . . . . . . 23
32030, 319syl 16 . . . . . . . . . . . . . . . . . . . . . 22
321320biimprd 215 . . . . . . . . . . . . . . . . . . . . 21
322 rsp 2758 . . . . . . . . . . . . . . . . . . . . 21
323321, 322syl9r 69 . . . . . . . . . . . . . . . . . . . 20
324323com13 76 . . . . . . . . . . . . . . . . . . 19
325318, 324syl 16 . . . . . . . . . . . . . . . . . 18
326325ex 424 . . . . . . . . . . . . . . . . 17
327326com24 83 . . . . . . . . . . . . . . . 16
328327imp 419 . . . . . . . . . . . . . . 15
3293283adant2 976 . . . . . . . . . . . . . 14
330329impcom 420 . . . . . . . . . . . . 13
331330rexlimiva 2817 . . . . . . . . . . . 12
332331ss2abi 3407 . . . . . . . . . . 11
33328, 332eqsstri 3370 . . . . . . . . . 10
334 sstr 3348 . . . . . . . . . 10
335333, 334mpan2 653 . . . . . . . . 9
336335sseld 3339 . . . . . . . 8
337 fvex 5734 . . . . . . . . 9
338 dmeq 5062 . . . . . . . . . . 11
339338eleq2d 2502 . . . . . . . . . 10
340 fveq1 5719 . . . . . . . . . . 11
341 fveq1 5719 . . . . . . . . . . . 12
342341fveq2d 5724 . . . . . . . . . . 11
343340, 342eleq12d 2503 . . . . . . . . . 10
344339, 343imbi12d 312 . . . . . . . . 9
345337, 344elab 3074 . . . . . . . 8
346336, 345syl6ib 218 . . . . . . 7
347302, 306, 315, 346syl3c 59 . . . . . 6
348211adantr 452 . . . . . . . 8
349 elssuni 4035 . . . . . . . . . 10
350305, 349syl 16 . . . . . . . . 9
351350adantlr 696 . . . . . . . 8
352 funssfv 5738 . . . . . . . 8
353348, 351, 315, 352syl3anc 1184 . . . . . . 7
354217sseld 3339 . . . . . . . . . . . . . . . 16
355338eleq2d 2502 . . . . . . . . . . . . . . . . . 18
356338eleq1d 2501 . . . . . . . . . . . . . . . . . 18
357355, 356anbi12d 692 . . . . . . . . . . . . . . . . 17
358337, 357elab 3074 . . . . . . . . . . . . . . . 16
359354, 358syl6ib 218 . . . . . . . . . . . . . . 15
360359adantr 452 . . . . . . . . . . . . . 14
361305, 360mpd 15 . . . . . . . . . . . . 13
362361simprd 450 . . . . . . . . . . . 12
363 nnord 4845 . . . . . . . . . . . 12
364362, 363syl 16 . . . . . . . . . . 11
365 ordtr 4587 . . . . . . . . . . 11
366 trsuc 4658 . . . . . . . . . . . 12
367366ex 424 . . . . . . . . . . 11
368364, 365, 3673syl 19 . . . . . . . . . 10
369368adantlr 696 . . . . . . . . 9
370315, 369mpd 15 . . . . . . . 8
371 funssfv 5738 . . . . . . . 8
372348, 351, 370, 371syl3anc 1184 . . . . . . 7
373 simpl 444 . . . . . . . 8
374 simpr 448 . . . . . . . . 9
375374fveq2d 5724 . . . . . . . 8
376373, 375eleq12d 2503 . . . . . . 7
377353, 372, 376syl2anc 643 . . . . . 6
378347, 377mpbird 224 . . . . 5
379378ex 424 . . . 4
380301, 379ralrimi 2779 . . 3
381 vex 2951 . . . . . 6
382381rnex 5125 . . . . 5
383382uniex 4697 . . . 4
384 feq1 5568 . . . . 5
385 fveq1 5719 . . . . . 6
386385eqeq1d 2443 . . . . 5
387 fveq1 5719 . . . . . . 7
388 fveq1 5719 . . . . . . . 8
389388fveq2d 5724 . . . . . . 7
390387, 389eleq12d 2503 . . . . . 6
391390ralbidv 2717 . . . . 5
392384, 386, 3913anbi123d 1254 . . . 4
393383, 392spcev 3035 . . 3
394276, 298, 380, 393syl3anc 1184 . 2
395394exlimiv 1644 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wo 358   wa 359   w3o 935   w3a 936  wex 1550   wceq 1652   wcel 1725  cab 2421  wral 2697  wrex 2698  crab 2701  cvv 2948   wss 3312  c0 3620  cop 3809  cuni 4007  ciun 4085   cmpt 4258   wtr 4294   word 4572   csuc 4575  com 4837   cdm 4870   crn 4871   cres 4872   wfun 5440   wfn 5441  wf 5442  cfv 5446 This theorem is referenced by:  axdc3lem4  8325 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-dc 8318 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-fv 5454  df-1o 6716
 Copyright terms: Public domain W3C validator