Definition df-cnf 8442

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

Assertion

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

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

Detailed syntax breakdown of Definition df-cnf

Step	Hyp	Ref	Expression
1		ccnf 8441	. 2 class CNF
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		con0 5640	. . 3 class On
5		vf	. . . 4 setvar 𝑓
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1474	. . . . . 6 class 𝑔
8		c0 3874	. . . . . 6 class ∅
9		cfsupp 8158	. . . . . 6 class finSupp
10	7, 8, 9	wbr 4583	. . . . 5 wff 𝑔 finSupp ∅
11	2	cv 1474	. . . . . 6 class 𝑥
12	3	cv 1474	. . . . . 6 class 𝑦
13		cmap 7744	. . . . . 6 class ↑𝑚
14	11, 12, 13	co 6549	. . . . 5 class (𝑥 ↑𝑚 𝑦)
15	10, 6, 14	crab 2900	. . . 4 class {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅}
16		vh	. . . . 5 setvar ℎ
17	5	cv 1474	. . . . . . 7 class 𝑓
18		csupp 7182	. . . . . . 7 class supp
19	17, 8, 18	co 6549	. . . . . 6 class (𝑓 supp ∅)
20		cep 4947	. . . . . 6 class E
21	19, 20	coi 8297	. . . . 5 class OrdIso( E , (𝑓 supp ∅))
22	16	cv 1474	. . . . . . 7 class ℎ
23	22	cdm 5038	. . . . . 6 class dom ℎ
24		vk	. . . . . . . 8 setvar 𝑘
25		vz	. . . . . . . 8 setvar 𝑧
26		cvv 3173	. . . . . . . 8 class V
27	24	cv 1474	. . . . . . . . . . . 12 class 𝑘
28	27, 22	cfv 5804	. . . . . . . . . . 11 class (ℎ‘𝑘)
29		coe 7446	. . . . . . . . . . 11 class ↑𝑜
30	11, 28, 29	co 6549	. . . . . . . . . 10 class (𝑥 ↑𝑜 (ℎ‘𝑘))
31	28, 17	cfv 5804	. . . . . . . . . 10 class (𝑓‘(ℎ‘𝑘))
32		comu 7445	. . . . . . . . . 10 class ·𝑜
33	30, 31, 32	co 6549	. . . . . . . . 9 class ((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘)))
34	25	cv 1474	. . . . . . . . 9 class 𝑧
35		coa 7444	. . . . . . . . 9 class +𝑜
36	33, 34, 35	co 6549	. . . . . . . 8 class (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)
37	24, 25, 26, 26, 36	cmpt2 6551	. . . . . . 7 class (𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧))
38	37, 8	cseqom 7429	. . . . . 6 class seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)
39	23, 38	cfv 5804	. . . . 5 class (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ)
40	16, 21, 39	csb 3499	. . . 4 class ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ)
41	5, 15, 40	cmpt 4643	. . 3 class (𝑓 ∈ {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ))
42	2, 3, 4, 4, 41	cmpt2 6551	. 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ)))
43	1, 42	wceq 1475	1 wff CNF = (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ)))

This definition is referenced by:  cantnffval  8443