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

Definition df-cnf 7617
 Description: Define the Cantor normal form function, which takes as input a finitely supported function from to and outputs the corresponding member of the ordinal exponential . The content of the original Cantor Normal Form theorem is that for this function is a bijection onto for any ordinal (or, since the function restricts naturally to different ordinals, the statement that the composite function is a bijection to ). More can be said about the function, however, and in particular it is an order isomorphism for a certain easily defined well-ordering of the finitely supported functions, which gives an alternate definition cantnffval2 7651 of this function in terms of df-oi 7479. (Contributed by Mario Carneiro, 25-May-2015.)
Assertion
Ref Expression
df-cnf CNF OrdIso seq𝜔
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-cnf
StepHypRef Expression
1 ccnf 7616 . 2 CNF
2 vx . . 3
3 vy . . 3
4 con0 4581 . . 3
5 vf . . . 4
6 vg . . . . . . . . 9
76cv 1651 . . . . . . . 8
87ccnv 4877 . . . . . . 7
9 cvv 2956 . . . . . . . 8
10 c1o 6717 . . . . . . . 8
119, 10cdif 3317 . . . . . . 7
128, 11cima 4881 . . . . . 6
13 cfn 7109 . . . . . 6
1412, 13wcel 1725 . . . . 5
152cv 1651 . . . . . 6
163cv 1651 . . . . . 6
17 cmap 7018 . . . . . 6
1815, 16, 17co 6081 . . . . 5
1914, 6, 18crab 2709 . . . 4
20 vh . . . . 5
215cv 1651 . . . . . . . 8
2221ccnv 4877 . . . . . . 7
2322, 11cima 4881 . . . . . 6
24 cep 4492 . . . . . 6
2523, 24coi 7478 . . . . 5 OrdIso
2620cv 1651 . . . . . . 7
2726cdm 4878 . . . . . 6
28 vk . . . . . . . 8
29 vz . . . . . . . 8
3028cv 1651 . . . . . . . . . . . 12
3130, 26cfv 5454 . . . . . . . . . . 11
32 coe 6723 . . . . . . . . . . 11
3315, 31, 32co 6081 . . . . . . . . . 10
3431, 21cfv 5454 . . . . . . . . . 10
35 comu 6722 . . . . . . . . . 10
3633, 34, 35co 6081 . . . . . . . . 9
3729cv 1651 . . . . . . . . 9
38 coa 6721 . . . . . . . . 9
3936, 37, 38co 6081 . . . . . . . 8
4028, 29, 9, 9, 39cmpt2 6083 . . . . . . 7
41 c0 3628 . . . . . . 7
4240, 41cseqom 6704 . . . . . 6 seq𝜔
4327, 42cfv 5454 . . . . 5 seq𝜔
4420, 25, 43csb 3251 . . . 4 OrdIso seq𝜔
455, 19, 44cmpt 4266 . . 3 OrdIso seq𝜔
462, 3, 4, 4, 45cmpt2 6083 . 2 OrdIso seq𝜔
471, 46wceq 1652 1 CNF OrdIso seq𝜔
 Colors of variables: wff set class This definition is referenced by:  cantnffval  7618
 Copyright terms: Public domain W3C validator