Definition df-cnf 9420

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 𝑥 ↑_o 𝑦. The content of the original Cantor Normal Form theorem is that for 𝑥 = ω this function is a bijection onto ω ↑_o 𝑦 for any ordinal 𝑦 (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 9453 of this function in terms of df-oi 9269. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)

Assertion

Ref	Expression
df-cnf	⊢ CNF = (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑m 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ)))

Distinct variable group:   𝑥,𝑦,𝑓,𝑔,ℎ,𝑘,𝑧

Detailed syntax breakdown of Definition df-cnf

Step	Hyp	Ref	Expression
1		ccnf 9419	. 2 class CNF
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		con0 6266	. . 3 class On
5		vf	. . . 4 setvar 𝑓
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1538	. . . . . 6 class 𝑔
8		c0 4256	. . . . . 6 class ∅
9		cfsupp 9128	. . . . . 6 class finSupp
10	7, 8, 9	wbr 5074	. . . . 5 wff 𝑔 finSupp ∅
11	2	cv 1538	. . . . . 6 class 𝑥
12	3	cv 1538	. . . . . 6 class 𝑦
13		cmap 8615	. . . . . 6 class ↑m
14	11, 12, 13	co 7275	. . . . 5 class (𝑥 ↑m 𝑦)
15	10, 6, 14	crab 3068	. . . 4 class {𝑔 ∈ (𝑥 ↑m 𝑦) ∣ 𝑔 finSupp ∅}
16		vh	. . . . 5 setvar ℎ
17	5	cv 1538	. . . . . . 7 class 𝑓
18		csupp 7977	. . . . . . 7 class supp
19	17, 8, 18	co 7275	. . . . . 6 class (𝑓 supp ∅)
20		cep 5494	. . . . . 6 class E
21	19, 20	coi 9268	. . . . 5 class OrdIso( E , (𝑓 supp ∅))
22	16	cv 1538	. . . . . . 7 class ℎ
23	22	cdm 5589	. . . . . 6 class dom ℎ
24		vk	. . . . . . . 8 setvar 𝑘
25		vz	. . . . . . . 8 setvar 𝑧
26		cvv 3432	. . . . . . . 8 class V
27	24	cv 1538	. . . . . . . . . . . 12 class 𝑘
28	27, 22	cfv 6433	. . . . . . . . . . 11 class (ℎ‘𝑘)
29		coe 8296	. . . . . . . . . . 11 class ↑o
30	11, 28, 29	co 7275	. . . . . . . . . 10 class (𝑥 ↑o (ℎ‘𝑘))
31	28, 17	cfv 6433	. . . . . . . . . 10 class (𝑓‘(ℎ‘𝑘))
32		comu 8295	. . . . . . . . . 10 class ·o
33	30, 31, 32	co 7275	. . . . . . . . 9 class ((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘)))
34	25	cv 1538	. . . . . . . . 9 class 𝑧
35		coa 8294	. . . . . . . . 9 class +o
36	33, 34, 35	co 7275	. . . . . . . 8 class (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)
37	24, 25, 26, 26, 36	cmpo 7277	. . . . . . 7 class (𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧))
38	37, 8	cseqom 8278	. . . . . 6 class seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)
39	23, 38	cfv 6433	. . . . 5 class (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ)
40	16, 21, 39	csb 3832	. . . 4 class ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ)
41	5, 15, 40	cmpt 5157	. . 3 class (𝑓 ∈ {𝑔 ∈ (𝑥 ↑m 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ))
42	2, 3, 4, 4, 41	cmpo 7277	. 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑m 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ)))
43	1, 42	wceq 1539	1 wff CNF = (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑m 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ)))

This definition is referenced by:  cantnffval  9421