Definition df-cnf 8559

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 8592 of this function in terms of df-oi 8415. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)

Assertion

Ref	Expression
df-cnf	|- CNF = ( x e. On , y e. On |-> ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )

Distinct variable group:   x, y, f, g, h, k, z

Detailed syntax breakdown of Definition df-cnf

Step	Hyp	Ref	Expression
1		ccnf 8558	. 2 class CNF
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		con0 5723	. . 3 class On
5		vf	. . . 4 setvar f
6		vg	. . . . . . 7 setvar g
7	6	cv 1482	. . . . . 6 class g
8		c0 3915	. . . . . 6 class (/)
9		cfsupp 8275	. . . . . 6 class finSupp
10	7, 8, 9	wbr 4653	. . . . 5 wff g finSupp (/)
11	2	cv 1482	. . . . . 6 class x
12	3	cv 1482	. . . . . 6 class y
13		cmap 7857	. . . . . 6 class ^m
14	11, 12, 13	co 6650	. . . . 5 class ( x ^m y )
15	10, 6, 14	crab 2916	. . . 4 class { g e. ( x ^m y ) | g finSupp (/) }
16		vh	. . . . 5 setvar h
17	5	cv 1482	. . . . . . 7 class f
18		csupp 7295	. . . . . . 7 class supp
19	17, 8, 18	co 6650	. . . . . 6 class ( f supp (/) )
20		cep 5028	. . . . . 6 class _E
21	19, 20	coi 8414	. . . . 5 class OrdIso ( _E , ( f supp (/) ) )
22	16	cv 1482	. . . . . . 7 class h
23	22	cdm 5114	. . . . . 6 class dom h
24		vk	. . . . . . . 8 setvar k
25		vz	. . . . . . . 8 setvar z
26		cvv 3200	. . . . . . . 8 class _V
27	24	cv 1482	. . . . . . . . . . . 12 class k
28	27, 22	cfv 5888	. . . . . . . . . . 11 class ( h ` k )
29		coe 7559	. . . . . . . . . . 11 class ^o
30	11, 28, 29	co 6650	. . . . . . . . . 10 class ( x ^o ( h ` k ) )
31	28, 17	cfv 5888	. . . . . . . . . 10 class ( f ` ( h ` k ) )
32		comu 7558	. . . . . . . . . 10 class .o
33	30, 31, 32	co 6650	. . . . . . . . 9 class ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) )
34	25	cv 1482	. . . . . . . . 9 class z
35		coa 7557	. . . . . . . . 9 class +o
36	33, 34, 35	co 6650	. . . . . . . 8 class ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z )
37	24, 25, 26, 26, 36	cmpt2 6652	. . . . . . 7 class ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) )
38	37, 8	cseqom 7542	. . . . . 6 class seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) )
39	23, 38	cfv 5888	. . . . 5 class (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h )
40	16, 21, 39	csb 3533	. . . 4 class [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h )
41	5, 15, 40	cmpt 4729	. . 3 class ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) )
42	2, 3, 4, 4, 41	cmpt2 6652	. 2 class ( x e. On , y e. On |-> ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
43	1, 42	wceq 1483	1 wff CNF = ( x e. On , y e. On |-> ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )

This definition is referenced by:  cantnffval  8560