This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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