This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnf ⊢ CNF
1 vx ⊢ 𝑥
2 con0 ⊢ On
3 vy ⊢ 𝑦
4 vf ⊢ 𝑓
5 vg ⊢ 𝑔
6 1 cv ⊢ 𝑥
7 cmap ⊢ ↑m
8 3 cv ⊢ 𝑦
9 6 8 7 co ⊢ ( 𝑥 ↑m 𝑦 )
10 5 cv ⊢ 𝑔
11 cfsupp ⊢ finSupp
12 c0 ⊢ ∅
13 10 12 11 wbr ⊢ 𝑔 finSupp ∅
14 13 5 9 crab ⊢ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ }
15 cep ⊢ E
16 4 cv ⊢ 𝑓
17 csupp ⊢ supp
18 16 12 17 co ⊢ ( 𝑓 supp ∅ )
19 18 15 coi ⊢ OrdIso ( E , ( 𝑓 supp ∅ ) )
20 vh ⊢ ℎ
21 vk ⊢ 𝑘
22 cvv ⊢ V
23 vz ⊢ 𝑧
24 coe ⊢ ↑o
25 20 cv ⊢ ℎ
26 21 cv ⊢ 𝑘
27 26 25 cfv ⊢ ( ℎ ‘ 𝑘 )
28 6 27 24 co ⊢ ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) )
29 comu ⊢ ·o
30 27 16 cfv ⊢ ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) )
31 28 30 29 co ⊢ ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) )
32 coa ⊢ +o
33 23 cv ⊢ 𝑧
34 31 33 32 co ⊢ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 )
35 21 23 22 22 34 cmpo ⊢ ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) )
36 35 12 cseqom ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
37 25 cdm ⊢ dom ℎ
38 37 36 cfv ⊢ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ )
39 20 19 38 csb ⊢ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ )
40 4 14 39 cmpt ⊢ ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) )
41 1 3 2 2 40 cmpo ⊢ ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) )
42 0 41 wceq ⊢ CNF = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) )