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

Theorem cantnfp1lem3 7592
 Description: Lemma for cantnfp1 7593. (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.1 CNF
cantnfs.2
cantnfs.3
cantnfp1.4
cantnfp1.5
cantnfp1.6
cantnfp1.7
cantnfp1.f
cantnfp1.8
cantnfp1.o OrdIso
cantnfp1.h seq𝜔
cantnfp1.k OrdIso
cantnfp1.m seq𝜔
Assertion
Ref Expression
cantnfp1lem3 CNF CNF
Distinct variable groups:   ,,,   ,,,   ,,   ,,,   ,,,   ,,,   ,,   ,,,   ,,,   ,,,
Allowed substitution hints:   ()   (,,)   (,,)   ()

Proof of Theorem cantnfp1lem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.1 . . 3 CNF
2 cantnfs.2 . . 3
3 cantnfs.3 . . 3
4 cantnfp1.o . . 3 OrdIso
5 cantnfp1.4 . . . 4
6 cantnfp1.5 . . . 4
7 cantnfp1.6 . . . 4
8 cantnfp1.7 . . . 4
9 cantnfp1.f . . . 4
101, 2, 3, 5, 6, 7, 8, 9cantnfp1lem1 7590 . . 3
11 cantnfp1.h . . 3 seq𝜔
121, 2, 3, 4, 10, 11cantnfval 7579 . 2 CNF
13 cantnfp1.8 . . . 4
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 7591 . . 3
1514fveq2d 5691 . 2
161, 2, 3, 4, 10cantnfcl 7578 . . . . . . 7
1716simprd 450 . . . . . 6
1814, 17eqeltrrd 2479 . . . . 5
19 peano2b 4820 . . . . 5
2018, 19sylibr 204 . . . 4
211, 2, 3, 4, 10, 11cantnfsuc 7581 . . . 4
2220, 21mpdan 650 . . 3
23 cnvimass 5183 . . . . . . . . . . . . . . . . 17
247adantr 452 . . . . . . . . . . . . . . . . . . . 20
251, 2, 3cantnfs 7577 . . . . . . . . . . . . . . . . . . . . . . 23
265, 25mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22
2726simpld 446 . . . . . . . . . . . . . . . . . . . . 21
2827ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . 20
29 ifcl 3735 . . . . . . . . . . . . . . . . . . . 20
3024, 28, 29syl2anc 643 . . . . . . . . . . . . . . . . . . 19
3130, 9fmptd 5852 . . . . . . . . . . . . . . . . . 18
32 fdm 5554 . . . . . . . . . . . . . . . . . 18
3331, 32syl 16 . . . . . . . . . . . . . . . . 17
3423, 33syl5sseq 3356 . . . . . . . . . . . . . . . 16
353, 34ssexd 4310 . . . . . . . . . . . . . . 15
3616simpld 446 . . . . . . . . . . . . . . 15
374oiiso 7462 . . . . . . . . . . . . . . 15
3835, 36, 37syl2anc 643 . . . . . . . . . . . . . 14
39 isof1o 6004 . . . . . . . . . . . . . 14
4038, 39syl 16 . . . . . . . . . . . . 13
41 f1ocnv 5646 . . . . . . . . . . . . 13
42 f1of 5633 . . . . . . . . . . . . 13
4340, 41, 423syl 19 . . . . . . . . . . . 12
44 iftrue 3705 . . . . . . . . . . . . . . . . 17
4544, 9fvmptg 5763 . . . . . . . . . . . . . . . 16
466, 7, 45syl2anc 643 . . . . . . . . . . . . . . 15
47 onelon 4566 . . . . . . . . . . . . . . . . . 18
482, 7, 47syl2anc 643 . . . . . . . . . . . . . . . . 17
49 on0eln0 4596 . . . . . . . . . . . . . . . . 17
5048, 49syl 16 . . . . . . . . . . . . . . . 16
5113, 50mpbid 202 . . . . . . . . . . . . . . 15
5246, 51eqnetrd 2585 . . . . . . . . . . . . . 14
53 fvex 5701 . . . . . . . . . . . . . . 15
54 dif1o 6703 . . . . . . . . . . . . . . 15
5553, 54mpbiran 885 . . . . . . . . . . . . . 14
5652, 55sylibr 204 . . . . . . . . . . . . 13
57 ffn 5550 . . . . . . . . . . . . . 14
58 elpreima 5809 . . . . . . . . . . . . . 14
5931, 57, 583syl 19 . . . . . . . . . . . . 13
606, 56, 59mpbir2and 889 . . . . . . . . . . . 12
6143, 60ffvelrnd 5830 . . . . . . . . . . 11
62 elssuni 4003 . . . . . . . . . . 11
6361, 62syl 16 . . . . . . . . . 10
644oicl 7454 . . . . . . . . . . . 12
65 ordelon 4565 . . . . . . . . . . . 12
6664, 61, 65sylancr 645 . . . . . . . . . . 11
67 nnon 4810 . . . . . . . . . . . 12
6820, 67syl 16 . . . . . . . . . . 11
69 ontri1 4575 . . . . . . . . . . 11
7066, 68, 69syl2anc 643 . . . . . . . . . 10
7163, 70mpbid 202 . . . . . . . . 9
72 sucidg 4619 . . . . . . . . . . . . . 14
7320, 72syl 16 . . . . . . . . . . . . 13
7473, 14eleqtrrd 2481 . . . . . . . . . . . 12
75 isorel 6005 . . . . . . . . . . . 12
7638, 74, 61, 75syl12anc 1182 . . . . . . . . . . 11
77 fvex 5701 . . . . . . . . . . . 12
7877epelc 4456 . . . . . . . . . . 11
79 fvex 5701 . . . . . . . . . . . 12
8079epelc 4456 . . . . . . . . . . 11
8176, 78, 803bitr3g 279 . . . . . . . . . 10
82 f1ocnvfv2 5974 . . . . . . . . . . . 12
8340, 60, 82syl2anc 643 . . . . . . . . . . 11
8483eleq2d 2471 . . . . . . . . . 10
8581, 84bitrd 245 . . . . . . . . 9
8671, 85mtbid 292 . . . . . . . 8
878sseld 3307 . . . . . . . . . 10
88 onss 4730 . . . . . . . . . . . . . . . 16
893, 88syl 16 . . . . . . . . . . . . . . 15
9034, 89sstrd 3318 . . . . . . . . . . . . . 14
914oif 7455 . . . . . . . . . . . . . . . 16
9291ffvelrni 5828 . . . . . . . . . . . . . . 15
9374, 92syl 16 . . . . . . . . . . . . . 14
9490, 93sseldd 3309 . . . . . . . . . . . . 13
95 eloni 4551 . . . . . . . . . . . . 13
9694, 95syl 16 . . . . . . . . . . . 12
97 ordn2lp 4561 . . . . . . . . . . . 12
9896, 97syl 16 . . . . . . . . . . 11
99 imnan 412 . . . . . . . . . . 11
10098, 99sylibr 204 . . . . . . . . . 10
10187, 100syld 42 . . . . . . . . 9
102 onelon 4566 . . . . . . . . . . . . 13
1033, 6, 102syl2anc 643 . . . . . . . . . . . 12
104 eloni 4551 . . . . . . . . . . . 12
105103, 104syl 16 . . . . . . . . . . 11
106 ordirr 4559 . . . . . . . . . . 11
107105, 106syl 16 . . . . . . . . . 10
108 elsni 3798 . . . . . . . . . . . 12
109108eleq2d 2471 . . . . . . . . . . 11
110109notbid 286 . . . . . . . . . 10
111107, 110syl5ibrcom 214 . . . . . . . . 9
112 df1o2 6695 . . . . . . . . . . . . . 14
113112difeq2i 3422 . . . . . . . . . . . . 13
114113imaeq2i 5160 . . . . . . . . . . . 12
115 eldifi 3429 . . . . . . . . . . . . . . . 16
116115adantl 453 . . . . . . . . . . . . . . 15
1177adantr 452 . . . . . . . . . . . . . . . 16
118 fvex 5701 . . . . . . . . . . . . . . . 16
119 ifexg 3758 . . . . . . . . . . . . . . . 16
120117, 118, 119sylancl 644 . . . . . . . . . . . . . . 15
121 eqeq1 2410 . . . . . . . . . . . . . . . . 17
122 fveq2 5687 . . . . . . . . . . . . . . . . 17
123121, 122ifbieq2d 3719 . . . . . . . . . . . . . . . 16
124123, 9fvmptg 5763 . . . . . . . . . . . . . . 15
125116, 120, 124syl2anc 643 . . . . . . . . . . . . . 14
126 eldifn 3430 . . . . . . . . . . . . . . . . 17
127126adantl 453 . . . . . . . . . . . . . . . 16
128 elsn 3789 . . . . . . . . . . . . . . . . 17
129 elun2 3475 . . . . . . . . . . . . . . . . 17
130128, 129sylbir 205 . . . . . . . . . . . . . . . 16
131127, 130nsyl 115 . . . . . . . . . . . . . . 15
132 iffalse 3706 . . . . . . . . . . . . . . 15
133131, 132syl 16 . . . . . . . . . . . . . 14
134 ssun1 3470 . . . . . . . . . . . . . . . . 17
135 sscon 3441 . . . . . . . . . . . . . . . . 17
136134, 135ax-mp 8 . . . . . . . . . . . . . . . 16
137136sseli 3304 . . . . . . . . . . . . . . 15
138113imaeq2i 5160 . . . . . . . . . . . . . . . . 17
139 eqimss2 3361 . . . . . . . . . . . . . . . . 17
140138, 139mp1i 12 . . . . . . . . . . . . . . . 16
14127, 140suppssr 5823 . . . . . . . . . . . . . . 15
142137, 141sylan2 461 . . . . . . . . . . . . . 14
143125, 133, 1423eqtrd 2440 . . . . . . . . . . . . 13
14431, 143suppss 5822 . . . . . . . . . . . 12
145114, 144syl5eqss 3352 . . . . . . . . . . 11
146145, 93sseldd 3309 . . . . . . . . . 10
147 elun 3448 . . . . . . . . . 10
148146, 147sylib 189 . . . . . . . . 9
149101, 111, 148mpjaod 371 . . . . . . . 8
150 ioran 477 . . . . . . . 8
15186, 149, 150sylanbrc 646 . . . . . . 7
152 ordtri3 4577 . . . . . . . 8
15396, 105, 152syl2anc 643 . . . . . . 7
154151, 153mpbird 224 . . . . . 6
155154oveq2d 6056 . . . . 5
156154fveq2d 5691 . . . . . 6
157156, 46eqtrd 2436 . . . . 5
158155, 157oveq12d 6058 . . . 4
159 nnord 4812 . . . . . . . . 9
16020, 159syl 16 . . . . . . . 8
161 sssucid 4618 . . . . . . . . . 10
162161, 14syl5sseqr 3357 . . . . . . . . 9
163 f1ofo 5640 . . . . . . . . . . . . 13
16440, 163syl 16 . . . . . . . . . . . 12
165 foima 5617 . . . . . . . . . . . 12
166164, 165syl 16 . . . . . . . . . . 11
167 ffn 5550 . . . . . . . . . . . . . 14
16891, 167ax-mp 8 . . . . . . . . . . . . 13
169 fnsnfv 5745 . . . . . . . . . . . . 13
170168, 74, 169sylancr 645 . . . . . . . . . . . 12
171154sneqd 3787 . . . . . . . . . . . 12
172170, 171eqtr3d 2438 . . . . . . . . . . 11
173166, 172difeq12d 3426 . . . . . . . . . 10
174 ordirr 4559 . . . . . . . . . . . . . . . . 17
175160, 174syl 16 . . . . . . . . . . . . . . . 16
176 disjsn 3828 . . . . . . . . . . . . . . . 16
177175, 176sylibr 204 . . . . . . . . . . . . . . 15
178 disj3 3632 . . . . . . . . . . . . . . 15
179177, 178sylib 189 . . . . . . . . . . . . . 14
180 difun2 3667 . . . . . . . . . . . . . 14
181179, 180syl6eqr 2454 . . . . . . . . . . . . 13
182 df-suc 4547 . . . . . . . . . . . . . . 15
18314, 182syl6eq 2452 . . . . . . . . . . . . . 14
184183difeq1d 3424 . . . . . . . . . . . . 13
185181, 184eqtr4d 2439 . . . . . . . . . . . 12
186185imaeq2d 5162 . . . . . . . . . . 11
187 dff1o3 5639 . . . . . . . . . . . . 13
188187simprbi 451 . . . . . . . . . . . 12
189 imadif 5487 . . . . . . . . . . . 12
19040, 188, 1893syl 19 . . . . . . . . . . 11
191186, 190eqtrd 2436 . . . . . . . . . 10
1928, 107ssneldd 3311 . . . . . . . . . . . . 13
193 disjsn 3828 . . . . . . . . . . . . 13
194192, 193sylibr 204 . . . . . . . . . . . 12
195 fvex 5701 . . . . . . . . . . . . . . . . . . . . . 22
196 dif1o 6703 . . . . . . . . . . . . . . . . . . . . . 22
197195, 196mpbiran 885 . . . . . . . . . . . . . . . . . . . . 21
198 ffn 5550 . . . . . . . . . . . . . . . . . . . . . . . . 25
19927, 198syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
200 elpreima 5809 . . . . . . . . . . . . . . . . . . . . . . . 24
201199, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
2028sseld 3307 . . . . . . . . . . . . . . . . . . . . . . 23
203201, 202sylbird 227 . . . . . . . . . . . . . . . . . . . . . 22
2046, 203mpand 657 . . . . . . . . . . . . . . . . . . . . 21
205197, 204syl5bir 210 . . . . . . . . . . . . . . . . . . . 20
206205necon1bd 2635 . . . . . . . . . . . . . . . . . . 19
207107, 206mpd 15 . . . . . . . . . . . . . . . . . 18
208207adantr 452 . . . . . . . . . . . . . . . . 17
209 fveq2 5687 . . . . . . . . . . . . . . . . . 18
210209eqeq1d 2412 . . . . . . . . . . . . . . . . 17
211208, 210syl5ibrcom 214 . . . . . . . . . . . . . . . 16
212 eldifi 3429 . . . . . . . . . . . . . . . . . . . 20
213212adantl 453 . . . . . . . . . . . . . . . . . . 19
2147adantr 452 . . . . . . . . . . . . . . . . . . . 20
215214, 118, 119sylancl 644 . . . . . . . . . . . . . . . . . . 19
216213, 215, 124syl2anc 643 . . . . . . . . . . . . . . . . . 18
217 ssid 3327 . . . . . . . . . . . . . . . . . . . 20
218217a1i 11 . . . . . . . . . . . . . . . . . . 19
21931, 218suppssr 5823 . . . . . . . . . . . . . . . . . 18
220216, 219eqtr3d 2438 . . . . . . . . . . . . . . . . 17
221132eqeq1d 2412 . . . . . . . . . . . . . . . . 17
222220, 221syl5ibcom 212 . . . . . . . . . . . . . . . 16
223211, 222pm2.61d 152 . . . . . . . . . . . . . . 15
22427, 223suppss 5822 . . . . . . . . . . . . . 14
225224, 138, 1143sstr4g 3349 . . . . . . . . . . . . 13
226 reldisj 3631 . . . . . . . . . . . . 13
227225, 226syl 16 . . . . . . . . . . . 12
228194, 227mpbid 202 . . . . . . . . . . 11
229 uncom 3451 . . . . . . . . . . . . 13
230145, 229syl6sseq 3354 . . . . . . . . . . . 12
231 ssundif 3671 . . . . . . . . . . . 12
232230, 231sylib 189 . . . . . . . . . . 11
233228, 232eqssd 3325 . . . . . . . . . 10
234173, 191, 2333eqtr4rd 2447 . . . . . . . . 9
235 isores3 6014 . . . . . . . . 9
23638, 162, 234, 235syl3anc 1184 . . . . . . . 8
237 cantnfp1.k . . . . . . . . . . 11 OrdIso
2381, 2, 3, 237, 5cantnfcl 7578 . . . . . . . . . 10
239238simpld 446 . . . . . . . . 9
240 epse 4525 . . . . . . . . 9 Se
241237oieu 7464 . . . . . . . . 9 Se
242239, 240, 241sylancl 644 . . . . . . . 8
243160, 236, 242mpbi2and 888 . . . . . . 7
244243simpld 446 . . . . . 6
245244fveq2d 5691 . . . . 5
246 eleq1 2464 . . . . . . . . . 10
247 fveq2 5687 . . . . . . . . . . 11
248 fveq2 5687 . . . . . . . . . . . 12
249 0ex 4299 . . . . . . . . . . . . 13
250 cantnfp1.m . . . . . . . . . . . . . 14 seq𝜔
251250seqom0g 6672 . . . . . . . . . . . . 13
252249, 251ax-mp 8 . . . . . . . . . . . 12
253248, 252syl6eq 2452 . . . . . . . . . . 11
254247, 253eqeq12d 2418 . . . . . . . . . 10
255246, 254imbi12d 312 . . . . . . . . 9
256255imbi2d 308 . . . . . . . 8
257 eleq1 2464 . . . . . . . . . 10
258 fveq2 5687 . . . . . . . . . . 11
259 fveq2 5687 . . . . . . . . . . 11
260258, 259eqeq12d 2418 . . . . . . . . . 10
261257, 260imbi12d 312 . . . . . . . . 9
262261imbi2d 308 . . . . . . . 8
263 eleq1 2464 . . . . . . . . . 10
264 fveq2 5687 . . . . . . . . . . 11
265 fveq2 5687 . . . . . . . . . . 11
266264, 265eqeq12d 2418 . . . . . . . . . 10
267263, 266imbi12d 312 . . . . . . . . 9
268267imbi2d 308 . . . . . . . 8
269 eleq1 2464 . . . . . . . . . 10
270 fveq2 5687 . . . . . . . . . . 11
271 fveq2 5687 . . . . . . . . . . 11
272270, 271eqeq12d 2418 . . . . . . . . . 10
273269, 272imbi12d 312 . . . . . . . . 9
274273imbi2d 308 . . . . . . . 8
27511seqom0g 6672 . . . . . . . . . 10
276249, 275mp1i 12 . . . . . . . . 9
277276a1i 11 . . . . . . . 8
278 nnord 4812 . . . . . . . . . . . . . . . 16
27917, 278syl 16 . . . . . . . . . . . . . . 15
280 ordtr 4555 . . . . . . . . . . . . . . 15
281279, 280syl 16 . . . . . . . . . . . . . 14
282 trsuc 4625 . . . . . . . . . . . . . 14
283281, 282sylan 458 . . . . . . . . . . . . 13
284283ex 424 . . . . . . . . . . . 12
285284imim1d 71 . . . . . . . . . . 11
286 oveq2 6048 . . . . . . . . . . . . . 14
287 elnn 4814 . . . . . . . . . . . . . . . . . . 19
288287ancoms 440 . . . . . . . . . . . . . . . . . 18
28917, 288sylan 458 . . . . . . . . . . . . . . . . 17
290283, 289syldan 457 . . . . . . . . . . . . . . . 16
2911, 2, 3, 4, 10, 11cantnfsuc 7581 . . . . . . . . . . . . . . . 16
292290, 291syldan 457 . . . . . . . . . . . . . . 15
2931, 2, 3, 237, 5, 250cantnfsuc 7581 . . . . . . . . . . . . . . . . 17
294290, 293syldan 457 . . . . . . . . . . . . . . . 16
295243simprd 450 . . . . . . . . . . . . . . . . . . . . . 22
296295fveq1d 5689 . . . . . . . . . . . . . . . . . . . . 21
297296adantr 452 . . . . . . . . . . . . . . . . . . . 20
29814eleq2d 2471 . . . . . . . . . . . . . . . . . . . . . . 23
299298biimpa 471 . . . . . . . . . . . . . . . . . . . . . 22
300160adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
301 ordsucelsuc 4761 . . . . . . . . . . . . . . . . . . . . . . 23
302300, 301syl 16 . . . . . . . . . . . . . . . . . . . . . 22
303299, 302mpbird 224 . . . . . . . . . . . . . . . . . . . . 21
304 fvres 5704 . . . . . . . . . . . . . . . . . . . . 21
305303, 304syl 16 . . . . . . . . . . . . . . . . . . . 20
306297, 305eqtr3d 2438 . . . . . . . . . . . . . . . . . . 19
307306oveq2d 6056 . . . . . . . . . . . . . . . . . 18
308 cnvimass 5183 . . . . . . . . . . . . . . . . . . . . . . 23
309 fdm 5554 . . . . . . . . . . . . . . . . . . . . . . . 24
31027, 309syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
311308, 310syl5sseq 3356 . . . . . . . . . . . . . . . . . . . . . 22
312311adantr 452 . . . . . . . . . . . . . . . . . . . . 21
313244adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
314303, 313eleqtrd 2480 . . . . . . . . . . . . . . . . . . . . . 22
315237oif 7455 . . . . . . . . . . . . . . . . . . . . . . 23
316315ffvelrni 5828 . . . . . . . . . . . . . . . . . . . . . 22
317314, 316syl 16 . . . . . . . . . . . . . . . . . . . . 21
318312, 317sseldd 3309 . . . . . . . . . . . . . . . . . . . 20
3197adantr 452 . . . . . . . . . . . . . . . . . . . . 21
320 fvex 5701 . . . . . . . . . . . . . . . . . . . . 21
321 ifexg 3758 . . . . . . . . . . . . . . . . . . . . 21
322319, 320, 321sylancl 644 . . . . . . . . . . . . . . . . . . . 20
323 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . 22
324 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . 22
325323, 324ifbieq2d 3719 . . . . . . . . . . . . . . . . . . . . 21
326325, 9fvmptg 5763 . . . . . . . . . . . . . . . . . . . 20
327318, 322, 326syl2anc 643 . . . . . . . . . . . . . . . . . . 19
328306fveq2d 5691 . . . . . . . . . . . . . . . . . . 19
329192adantr 452 . . . . . . . . . . . . . . . . . . . . 21
330 nelneq 2502 . . . . . . . . . . . . . . . . . . . . 21
331317, 329, 330syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
332 iffalse 3706 . . . . . . . . . . . . . . . . . . . 20
333331, 332syl 16 . . . . . . . . . . . . . . . . . . 19
334327, 328, 3333eqtr3rd 2445 . . . . . . . . . . . . . . . . . 18
335307, 334oveq12d 6058 . . . . . . . . . . . . . . . . 17
336335oveq1d 6055 . . . . . . . . . . . . . . . 16
337294, 336eqtrd 2436 . . . . . . . . . . . . . . 15
338292, 337eqeq12d 2418 . . . . . . . . . . . . . 14
339286, 338syl5ibr 213 . . . . . . . . . . . . 13
340339ex 424 . . . . . . . . . . . 12
341340a2d 24 . . . . . . . . . . 11
342285, 341syld 42 . . . . . . . . . 10
343342a2i 13 . . . . . . . . 9
344343a1i 11 . . . . . . . 8
345256, 262, 268, 274, 277, 344finds 4830 . . . . . . 7
34620, 345mpcom 34 . . . . . 6
34774, 346mpd 15 . . . . 5
3481, 2, 3, 237, 5, 250cantnfval 7579 . . . . 5 CNF
349245, 347, 3483eqtr4d 2446 . . . 4 CNF
350158, 349oveq12d 6058 . . 3 CNF
35122, 350eqtrd 2436 . 2 CNF
35212, 15, 3513eqtrd 2440 1 CNF CNF
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   wceq 1649   wcel 1721   wne 2567  cvv 2916   cdif 3277   cun 3278   cin 3279   wss 3280  c0 3588  cif 3699  csn 3774  cuni 3975   class class class wbr 4172   cmpt 4226   wtr 4262   cep 4452   Se wse 4499   wwe 4500   word 4540  con0 4541   csuc 4543  com 4804  ccnv 4836   cdm 4837   cres 4839  cima 4840   wfun 5407   wfn 5408  wf 5409  wfo 5411  wf1o 5412  cfv 5413   wiso 5414  (class class class)co 6040   cmpt2 6042  seq𝜔cseqom 6663  c1o 6676   coa 6680   comu 6681   coe 6682  cfn 7068  OrdIsocoi 7434   CNF ccnf 7572 This theorem is referenced by:  cantnfp1  7593 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-seqom 6664  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-cnf 7573
 Copyright terms: Public domain W3C validator