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

Theorem cantnf 7641
 Description: The Cantor Normal Form theorem. The function CNF , which maps a finitely supported function from to to the sum over all indexes such that is nonzero, is an order isomorphism from the ordering of finitely supported functions to the set under the natural order. Setting and letting be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres 7625, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.1 CNF
cantnfs.2
cantnfs.3
oemapval.t
Assertion
Ref Expression
cantnf CNF
Distinct variable groups:   ,,,,   ,,,,   ,,,   ,,,
Allowed substitution hints:   ()   ()   (,,,)

Proof of Theorem cantnf
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 oemapval.t . . 3
51, 2, 3, 4oemapso 7630 . 2
6 oecl 6773 . . . . . 6
72, 3, 6syl2anc 643 . . . . 5
8 eloni 4583 . . . . 5
97, 8syl 16 . . . 4
10 ordwe 4586 . . . 4
119, 10syl 16 . . 3
12 weso 4565 . . 3
13 sopo 4512 . . 3
1411, 12, 133syl 19 . 2
151, 2, 3cantnff 7621 . . 3 CNF
16 frn 5589 . . . . 5 CNF CNF
1715, 16syl 16 . . . 4 CNF
18 onss 4763 . . . . . . . 8
197, 18syl 16 . . . . . . 7
2019sseld 3339 . . . . . 6
21 eleq1 2495 . . . . . . . . . 10
22 eleq1 2495 . . . . . . . . . 10 CNF CNF
2321, 22imbi12d 312 . . . . . . . . 9 CNF CNF
2423imbi2d 308 . . . . . . . 8 CNF CNF
25 r19.21v 2785 . . . . . . . . 9 CNF CNF
26 ordelss 4589 . . . . . . . . . . . . . . . . . . 19
279, 26sylan 458 . . . . . . . . . . . . . . . . . 18
2827sselda 3340 . . . . . . . . . . . . . . . . 17
29 pm5.5 327 . . . . . . . . . . . . . . . . 17 CNF CNF
3028, 29syl 16 . . . . . . . . . . . . . . . 16 CNF CNF
3130ralbidva 2713 . . . . . . . . . . . . . . 15 CNF CNF
32 dfss3 3330 . . . . . . . . . . . . . . 15 CNF CNF
3331, 32syl6bbr 255 . . . . . . . . . . . . . 14 CNF CNF
34 eleq1 2495 . . . . . . . . . . . . . . . 16 CNF CNF
352adantr 452 . . . . . . . . . . . . . . . . . 18 CNF
3635adantr 452 . . . . . . . . . . . . . . . . 17 CNF
373adantr 452 . . . . . . . . . . . . . . . . . 18 CNF
3837adantr 452 . . . . . . . . . . . . . . . . 17 CNF
39 simplrl 737 . . . . . . . . . . . . . . . . 17 CNF
40 simplrr 738 . . . . . . . . . . . . . . . . 17 CNF CNF
417adantr 452 . . . . . . . . . . . . . . . . . . . 20 CNF
42 simprl 733 . . . . . . . . . . . . . . . . . . . 20 CNF
43 onelon 4598 . . . . . . . . . . . . . . . . . . . 20
4441, 42, 43syl2anc 643 . . . . . . . . . . . . . . . . . . 19 CNF
45 on0eln0 4628 . . . . . . . . . . . . . . . . . . 19
4644, 45syl 16 . . . . . . . . . . . . . . . . . 18 CNF
4746biimpar 472 . . . . . . . . . . . . . . . . 17 CNF
48 eqid 2435 . . . . . . . . . . . . . . . . 17
49 eqid 2435 . . . . . . . . . . . . . . . . 17
50 eqid 2435 . . . . . . . . . . . . . . . . 17
51 eqid 2435 . . . . . . . . . . . . . . . . 17
521, 36, 38, 4, 39, 40, 47, 48, 49, 50, 51cantnflem4 7640 . . . . . . . . . . . . . . . 16 CNF CNF
53 fconstmpt 4913 . . . . . . . . . . . . . . . . . . . . . 22
5453mptpreima 5355 . . . . . . . . . . . . . . . . . . . . 21
55 neirr 2603 . . . . . . . . . . . . . . . . . . . . . . . 24
56 dif1o 6736 . . . . . . . . . . . . . . . . . . . . . . . . 25
5756simprbi 451 . . . . . . . . . . . . . . . . . . . . . . . 24
5855, 57mto 169 . . . . . . . . . . . . . . . . . . . . . . 23
5958rgenw 2765 . . . . . . . . . . . . . . . . . . . . . 22
60 rabeq0 3641 . . . . . . . . . . . . . . . . . . . . . 22
6159, 60mpbir 201 . . . . . . . . . . . . . . . . . . . . 21
6254, 61eqtr2i 2456 . . . . . . . . . . . . . . . . . . . 20
63 oieq2 7474 . . . . . . . . . . . . . . . . . . . 20 OrdIso OrdIso
6462, 63ax-mp 8 . . . . . . . . . . . . . . . . . . 19 OrdIso OrdIso
65 ne0i 3626 . . . . . . . . . . . . . . . . . . . . . . 23
66 ne0i 3626 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6766ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26 CNF
68 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6968neeq1d 2611 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7067, 69syl5ibcom 212 . . . . . . . . . . . . . . . . . . . . . . . . 25 CNF
7170necon2d 2648 . . . . . . . . . . . . . . . . . . . . . . . 24 CNF
72 on0eln0 4628 . . . . . . . . . . . . . . . . . . . . . . . . . 26
73 oe0m1 6757 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7472, 73bitr3d 247 . . . . . . . . . . . . . . . . . . . . . . . . 25
7537, 74syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 CNF
76 on0eln0 4628 . . . . . . . . . . . . . . . . . . . . . . . . 25
7735, 76syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 CNF
7871, 75, 773imtr4d 260 . . . . . . . . . . . . . . . . . . . . . . 23 CNF
7965, 78syl5 30 . . . . . . . . . . . . . . . . . . . . . 22 CNF
8079imp 419 . . . . . . . . . . . . . . . . . . . . 21 CNF
8180, 53fmptd 5885 . . . . . . . . . . . . . . . . . . . 20 CNF
82 0fin 7328 . . . . . . . . . . . . . . . . . . . . . 22
8362, 82eqeltrri 2506 . . . . . . . . . . . . . . . . . . . . 21
8483a1i 11 . . . . . . . . . . . . . . . . . . . 20 CNF
851, 2, 3cantnfs 7613 . . . . . . . . . . . . . . . . . . . . 21
8685adantr 452 . . . . . . . . . . . . . . . . . . . 20 CNF
8781, 84, 86mpbir2and 889 . . . . . . . . . . . . . . . . . . 19 CNF
88 eqid 2435 . . . . . . . . . . . . . . . . . . 19 seq𝜔 OrdIso OrdIso seq𝜔 OrdIso OrdIso
891, 35, 37, 64, 87, 88cantnfval 7615 . . . . . . . . . . . . . . . . . 18 CNF CNF seq𝜔 OrdIso OrdIso OrdIso
90 0ex 4331 . . . . . . . . . . . . . . . . . . . . . 22
91 we0 4569 . . . . . . . . . . . . . . . . . . . . . 22
92 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso OrdIso
9392oien 7499 . . . . . . . . . . . . . . . . . . . . . 22 OrdIso
9490, 91, 93mp2an 654 . . . . . . . . . . . . . . . . . . . . 21 OrdIso
95 en0 7162 . . . . . . . . . . . . . . . . . . . . 21 OrdIso OrdIso
9694, 95mpbi 200 . . . . . . . . . . . . . . . . . . . 20 OrdIso
9796fveq2i 5723 . . . . . . . . . . . . . . . . . . 19 seq𝜔 OrdIso OrdIso OrdIso seq𝜔 OrdIso OrdIso
9888seqom0g 6705 . . . . . . . . . . . . . . . . . . . 20 seq𝜔 OrdIso OrdIso
9990, 98ax-mp 8 . . . . . . . . . . . . . . . . . . 19 seq𝜔 OrdIso OrdIso
10097, 99eqtri 2455 . . . . . . . . . . . . . . . . . 18 seq𝜔 OrdIso OrdIso OrdIso
10189, 100syl6eq 2483 . . . . . . . . . . . . . . . . 17 CNF CNF
10215adantr 452 . . . . . . . . . . . . . . . . . . 19 CNF CNF
103 ffn 5583 . . . . . . . . . . . . . . . . . . 19 CNF CNF
104102, 103syl 16 . . . . . . . . . . . . . . . . . 18 CNF CNF
105 fnfvelrn 5859 . . . . . . . . . . . . . . . . . 18 CNF CNF CNF
106104, 87, 105syl2anc 643 . . . . . . . . . . . . . . . . 17 CNF CNF CNF
107101, 106eqeltrrd 2510 . . . . . . . . . . . . . . . 16 CNF CNF
10834, 52, 107pm2.61ne 2673 . . . . . . . . . . . . . . 15 CNF CNF
109108expr 599 . . . . . . . . . . . . . 14 CNF CNF
11033, 109sylbid 207 . . . . . . . . . . . . 13 CNF CNF
111110ex 424 . . . . . . . . . . . 12 CNF CNF
112111com23 74 . . . . . . . . . . 11 CNF CNF
113112a2i 13 . . . . . . . . . 10 CNF CNF
114113a1i 11 . . . . . . . . 9 CNF CNF
11525, 114syl5bi 209 . . . . . . . 8 CNF CNF
11624, 115tfis2 4828 . . . . . . 7 CNF
117116com3l 77 . . . . . 6 CNF
11820, 117mpdd 38 . . . . 5 CNF
119118ssrdv 3346 . . . 4 CNF
12017, 119eqssd 3357 . . 3 CNF
121 dffo2 5649 . . 3 CNF CNF CNF
12215, 120, 121sylanbrc 646 . 2 CNF
1232adantr 452 . . . . . 6
1243adantr 452 . . . . . 6
125 fveq2 5720 . . . . . . . . . . . 12
126 fveq2 5720 . . . . . . . . . . . 12
127125, 126eleq12d 2503 . . . . . . . . . . 11
128 eleq1 2495 . . . . . . . . . . . . 13
129128imbi1d 309 . . . . . . . . . . . 12
130129ralbidv 2717 . . . . . . . . . . 11
131127, 130anbi12d 692 . . . . . . . . . 10
132131cbvrexv 2925 . . . . . . . . 9
133 fveq1 5719 . . . . . . . . . . . 12
134 fveq1 5719 . . . . . . . . . . . 12
135 eleq12 2497 . . . . . . . . . . . 12
136133, 134, 135syl2an 464 . . . . . . . . . . 11
137 fveq1 5719 . . . . . . . . . . . . . 14
138 fveq1 5719 . . . . . . . . . . . . . 14
139137, 138eqeqan12d 2450 . . . . . . . . . . . . 13
140139imbi2d 308 . . . . . . . . . . . 12
141140ralbidv 2717 . . . . . . . . . . 11
142136, 141anbi12d 692 . . . . . . . . . 10
143142rexbidv 2718 . . . . . . . . 9
144132, 143syl5bb 249 . . . . . . . 8
145144cbvopabv 4269 . . . . . . 7
1464, 145eqtri 2455 . . . . . 6
147 simprll 739 . . . . . 6
148 simprlr 740 . . . . . 6
149 simprr 734 . . . . . 6
150 eqid 2435 . . . . . 6
151 eqid 2435 . . . . . 6 OrdIso OrdIso
152 eqid 2435 . . . . . 6 seq𝜔 OrdIso OrdIso seq𝜔 OrdIso OrdIso
1531, 123, 124, 146, 147, 148, 149, 150, 151, 152cantnflem1 7637 . . . . 5 CNF CNF
154 fvex 5734 . . . . . 6 CNF
155154epelc 4488 . . . . 5 CNF CNF CNF CNF
156153, 155sylibr 204 . . . 4 CNF CNF
157156expr 599 . . 3 CNF CNF
158157ralrimivva 2790 . 2 CNF CNF
159 soisoi 6040 . 2 CNF CNF CNF CNF
1605, 14, 122, 158, 159syl22anc 1185 1 CNF
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wceq 1652   wcel 1725   wne 2598  wral 2697  wrex 2698  crab 2701  cvv 2948   cdif 3309   wss 3312  c0 3620  csn 3806  cop 3809  cuni 4007  cint 4042   class class class wbr 4204  copab 4257   cep 4484   wpo 4493   wor 4494   wwe 4532   word 4572  con0 4573   cxp 4868  ccnv 4869   cdm 4870   crn 4871  cima 4873  cio 5408   wfn 5441  wf 5442  wfo 5444  cfv 5446   wiso 5447  (class class class)co 6073   cmpt2 6075  c1st 6339  c2nd 6340  seq𝜔cseqom 6696  c1o 6709   coa 6713   comu 6714   coe 6715   cen 7098  cfn 7101  OrdIsocoi 7470   CNF ccnf 7608 This theorem is referenced by:  oemapwe  7642  cantnffval2  7643  cantnff1o  7644 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-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693 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-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  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-int 4043  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-se 4534  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-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-seqom 6697  df-1o 6716  df-2o 6717  df-oadd 6720  df-omul 6721  df-oexp 6722  df-er 6897  df-map 7012  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-oi 7471  df-cnf 7609
 Copyright terms: Public domain W3C validator