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

Definition df-cnf 7573
 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 7607 of this function in terms of df-oi 7435. (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 7572 . 2 CNF
2 vx . . 3
3 vy . . 3
4 con0 4541 . . 3
5 vf . . . 4
6 vg . . . . . . . . 9
76cv 1648 . . . . . . . 8
87ccnv 4836 . . . . . . 7
9 cvv 2916 . . . . . . . 8
10 c1o 6676 . . . . . . . 8
119, 10cdif 3277 . . . . . . 7
128, 11cima 4840 . . . . . 6
13 cfn 7068 . . . . . 6
1412, 13wcel 1721 . . . . 5
152cv 1648 . . . . . 6
163cv 1648 . . . . . 6
17 cmap 6977 . . . . . 6
1815, 16, 17co 6040 . . . . 5
1914, 6, 18crab 2670 . . . 4
20 vh . . . . 5
215cv 1648 . . . . . . . 8
2221ccnv 4836 . . . . . . 7
2322, 11cima 4840 . . . . . 6
24 cep 4452 . . . . . 6
2523, 24coi 7434 . . . . 5 OrdIso
2620cv 1648 . . . . . . 7
2726cdm 4837 . . . . . 6
28 vk . . . . . . . 8
29 vz . . . . . . . 8
3028cv 1648 . . . . . . . . . . . 12
3130, 26cfv 5413 . . . . . . . . . . 11
32 coe 6682 . . . . . . . . . . 11
3315, 31, 32co 6040 . . . . . . . . . 10
3431, 21cfv 5413 . . . . . . . . . 10
35 comu 6681 . . . . . . . . . 10
3633, 34, 35co 6040 . . . . . . . . 9
3729cv 1648 . . . . . . . . 9
38 coa 6680 . . . . . . . . 9
3936, 37, 38co 6040 . . . . . . . 8
4028, 29, 9, 9, 39cmpt2 6042 . . . . . . 7
41 c0 3588 . . . . . . 7
4240, 41cseqom 6663 . . . . . 6 seq𝜔
4327, 42cfv 5413 . . . . 5 seq𝜔
4420, 25, 43csb 3211 . . . 4 OrdIso seq𝜔
455, 19, 44cmpt 4226 . . 3 OrdIso seq𝜔
462, 3, 4, 4, 45cmpt2 6042 . 2 OrdIso seq𝜔
471, 46wceq 1649 1 CNF OrdIso seq𝜔
 Colors of variables: wff set class This definition is referenced by:  cantnffval  7574
 Copyright terms: Public domain W3C validator