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 ∈ x y | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnf class CNF
1 vx setvar x
2 con0 class On
3 vy setvar y
4 vf setvar f
5 vg setvar g
6 1 cv setvar x
7 cmap class ↑ 𝑚
8 3 cv setvar y
9 6 8 7 co class x y
10 5 cv setvar g
11 cfsupp class finSupp
12 c0 class ∅
13 10 12 11 wbr wff finSupp ∅⁡ g
14 13 5 9 crab class g ∈ x y | finSupp ∅⁡ g
15 cep class E
16 4 cv setvar f
17 csupp class supp
18 16 12 17 co class supp ∅⁡ f
19 18 15 coi class OrdIso E f supp ∅
20 vh setvar h
21 vk setvar k
22 cvv class V
23 vz setvar z
24 coe class ↑ 𝑜
25 20 cv setvar h
26 21 cv setvar k
27 26 25 cfv class h ⁡ k
28 6 27 24 co class x ↑ 𝑜 h ⁡ k
29 comu class ⋅ 𝑜
30 27 16 cfv class f ⁡ h ⁡ k
31 28 30 29 co class x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k
32 coa class + 𝑜
33 23 cv setvar z
34 31 33 32 co class x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z
35 21 23 22 22 34 cmpo class k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z
36 35 12 cseqom class seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅
37 25 cdm class dom ⁡ h
38 37 36 cfv class seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
39 20 19 38 csb class ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
40 4 14 39 cmpt class f ∈ g ∈ x y | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
41 1 3 2 2 40 cmpo class x ∈ On , y ∈ On ⟼ f ∈ g ∈ x y | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
42 0 41 wceq wff CNF = x ∈ On , y ∈ On ⟼ f ∈ g ∈ x y | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h