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 ℎ ) ) )