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 e. On , y e. On |-> ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnf	|- CNF
1		vx	|- x
2		con0	|- On
3		vy	|- y
4		vf	|- f
5		vg	|- g
6	1	cv	|- x
7		cmap	|- ^m
8	3	cv	|- y
9	6 8 7	co	|- ( x ^m y )
10	5	cv	|- g
11		cfsupp	|- finSupp
12		c0	|- (/)
13	10 12 11	wbr	|- g finSupp (/)
14	13 5 9	crab	|- { g e. ( x ^m y ) | g finSupp (/) }
15		cep	|- _E
16	4	cv	|- f
17		csupp	|- supp
18	16 12 17	co	|- ( f supp (/) )
19	18 15	coi	|- OrdIso ( _E , ( f supp (/) ) )
20		vh	|- h
21		vk	|- k
22		cvv	|- _V
23		vz	|- z
24		coe	|- ^o
25	20	cv	|- h
26	21	cv	|- k
27	26 25	cfv	|- ( h ` k )
28	6 27 24	co	|- ( x ^o ( h ` k ) )
29		comu	|- .o
30	27 16	cfv	|- ( f ` ( h ` k ) )
31	28 30 29	co	|- ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) )
32		coa	|- +o
33	23	cv	|- z
34	31 33 32	co	|- ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z )
35	21 23 22 22 34	cmpo	|- ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) )
36	35 12	cseqom	|- seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) )
37	25	cdm	|- dom h
38	37 36	cfv	|- ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h )
39	20 19 38	csb	|- [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h )
40	4 14 39	cmpt	|- ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) )
41	1 3 2 2 40	cmpo	|- ( x e. On , y e. On |-> ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
42	0 41	wceq	|- CNF = ( x e. On , y e. On |-> ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )