Metamath Proof Explorer

Definition df-cnf

Description: Define the Cantor normal form function, which takes as input a finitely supported function from y to x and outputs the corresponding member of the ordinal exponential x ^o y . The content of the original Cantor Normal Form theorem is that for x =om this function is a bijection onto om ^o y for any ordinal y (or, since the function restricts naturally to different ordinals, the statement that the composite function is a bijection to On ). 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 of this function in terms of df-oi . (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Assertion df-cnf ⊢CNF=x∈On,y∈On⟼f∈g∈xy|finSupp∅⁡g⟼⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼x↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnf classCNF
1 vx setvarx
2 con0 classOn
3 vy setvary
4 vf setvarf
5 vg setvarg
6 1 cv setvarx
7 cmap class↑𝑚
8 3 cv setvary
9 6 8 7 co classxy
10 5 cv setvarg
11 cfsupp classfinSupp
12 c0 class∅
13 10 12 11 wbr wfffinSupp∅⁡g
14 13 5 9 crab classg∈xy|finSupp∅⁡g
15 cep classE
16 4 cv setvarf
17 csupp classsupp
18 16 12 17 co classsupp∅⁡f
19 18 15 coi classOrdIsoEfsupp∅
20 vh setvarh
21 vk setvark
22 cvv classV
23 vz setvarz
24 coe class↑𝑜
25 20 cv setvarh
26 21 cv setvark
27 26 25 cfv classh⁡k
28 6 27 24 co classx↑𝑜h⁡k
29 comu class⋅𝑜
30 27 16 cfv classf⁡h⁡k
31 28 30 29 co classx↑𝑜h⁡k⋅𝑜f⁡h⁡k
32 coa class+𝑜
33 23 cv setvarz
34 31 33 32 co classx↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z
35 21 23 22 22 34 cmpo classk∈V,z∈V⟼x↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z
36 35 12 cseqom classseqωk∈V,z∈V⟼x↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅
37 25 cdm classdom⁡h
38 37 36 cfv classseqωk∈V,z∈V⟼x↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h
39 20 19 38 csb class⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼x↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h
40 4 14 39 cmpt classf∈g∈xy|finSupp∅⁡g⟼⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼x↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h
41 1 3 2 2 40 cmpo classx∈On,y∈On⟼f∈g∈xy|finSupp∅⁡g⟼⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼x↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h
42 0 41 wceq wffCNF=x∈On,y∈On⟼f∈g∈xy|finSupp∅⁡g⟼⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼x↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h