MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnf Unicode version

Definition df-cnf 7363
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 7397 of this function in terms of df-oi 7225. (Contributed by Mario Carneiro, 25-May-2015.)
Assertion
Ref Expression
df-cnf  |- CNF  =  ( x  e.  On , 
y  e.  On  |->  ( f  e.  { g  e.  ( x  ^m  y )  |  ( `' g " ( _V  \  1o ) )  e.  Fin }  |->  [_OrdIso (  _E  ,  ( `' f " ( _V 
\  1o ) ) )  /  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
StepHypRef Expression
1 ccnf 7362 . 2  class CNF
2 vx . . 3  set  x
3 vy . . 3  set  y
4 con0 4392 . . 3  class  On
5 vf . . . 4  set  f
6 vg . . . . . . . . 9  set  g
76cv 1622 . . . . . . . 8  class  g
87ccnv 4688 . . . . . . 7  class  `' g
9 cvv 2788 . . . . . . . 8  class  _V
10 c1o 6472 . . . . . . . 8  class  1o
119, 10cdif 3149 . . . . . . 7  class  ( _V 
\  1o )
128, 11cima 4692 . . . . . 6  class  ( `' g " ( _V 
\  1o ) )
13 cfn 6863 . . . . . 6  class  Fin
1412, 13wcel 1684 . . . . 5  wff  ( `' g " ( _V 
\  1o ) )  e.  Fin
152cv 1622 . . . . . 6  class  x
163cv 1622 . . . . . 6  class  y
17 cmap 6772 . . . . . 6  class  ^m
1815, 16, 17co 5858 . . . . 5  class  ( x  ^m  y )
1914, 6, 18crab 2547 . . . 4  class  { g  e.  ( x  ^m  y )  |  ( `' g " ( _V  \  1o ) )  e.  Fin }
20 vh . . . . 5  set  h
215cv 1622 . . . . . . . 8  class  f
2221ccnv 4688 . . . . . . 7  class  `' f
2322, 11cima 4692 . . . . . 6  class  ( `' f " ( _V 
\  1o ) )
24 cep 4303 . . . . . 6  class  _E
2523, 24coi 7224 . . . . 5  class OrdIso (  _E  ,  ( `' f
" ( _V  \  1o ) ) )
2620cv 1622 . . . . . . 7  class  h
2726cdm 4689 . . . . . 6  class  dom  h
28 vk . . . . . . . 8  set  k
29 vz . . . . . . . 8  set  z
3028cv 1622 . . . . . . . . . . . 12  class  k
3130, 26cfv 5255 . . . . . . . . . . 11  class  ( h `
 k )
32 coe 6478 . . . . . . . . . . 11  class  ^o
3315, 31, 32co 5858 . . . . . . . . . 10  class  ( x  ^o  ( h `  k ) )
3431, 21cfv 5255 . . . . . . . . . 10  class  ( f `
 ( h `  k ) )
35 comu 6477 . . . . . . . . . 10  class  .o
3633, 34, 35co 5858 . . . . . . . . 9  class  ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )
3729cv 1622 . . . . . . . . 9  class  z
38 coa 6476 . . . . . . . . 9  class  +o
3936, 37, 38co 5858 . . . . . . . 8  class  ( ( ( x  ^o  (
h `  k )
)  .o  ( f `
 ( h `  k ) ) )  +o  z )
4028, 29, 9, 9, 39cmpt2 5860 . . . . . . 7  class  ( k  e.  _V ,  z  e.  _V  |->  ( ( ( x  ^o  (
h `  k )
)  .o  ( f `
 ( h `  k ) ) )  +o  z ) )
41 c0 3455 . . . . . . 7  class  (/)
4240, 41cseqom 6459 . . . . . 6  class seq𝜔 ( ( k  e. 
_V ,  z  e. 
_V  |->  ( ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )  +o  z ) ) ,  (/) )
4327, 42cfv 5255 . . . . 5  class  (seq𝜔 ( ( k  e.  _V , 
z  e.  _V  |->  ( ( ( x  ^o  ( h `  k
) )  .o  (
f `  ( h `  k ) ) )  +o  z ) ) ,  (/) ) `  dom  h )
4420, 25, 43csb 3081 . . . 4  class  [_OrdIso (  _E  ,  ( `' f
" ( _V  \  1o ) ) )  /  h ]_ (seq𝜔 ( ( k  e. 
_V ,  z  e. 
_V  |->  ( ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )  +o  z ) ) ,  (/) ) `  dom  h
)
455, 19, 44cmpt 4077 . . 3  class  ( f  e.  { g  e.  ( x  ^m  y
)  |  ( `' g " ( _V 
\  1o ) )  e.  Fin }  |->  [_OrdIso (  _E  ,  ( `' f " ( _V 
\  1o ) ) )  /  h ]_ (seq𝜔 ( ( k  e. 
_V ,  z  e. 
_V  |->  ( ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )  +o  z ) ) ,  (/) ) `  dom  h
) )
462, 3, 4, 4, 45cmpt2 5860 . 2  class  ( x  e.  On ,  y  e.  On  |->  ( f  e.  { g  e.  ( x  ^m  y
)  |  ( `' g " ( _V 
\  1o ) )  e.  Fin }  |->  [_OrdIso (  _E  ,  ( `' f " ( _V 
\  1o ) ) )  /  h ]_ (seq𝜔 ( ( k  e. 
_V ,  z  e. 
_V  |->  ( ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )  +o  z ) ) ,  (/) ) `  dom  h
) ) )
471, 46wceq 1623 1  wff CNF  =  ( x  e.  On , 
y  e.  On  |->  ( f  e.  { g  e.  ( x  ^m  y )  |  ( `' g " ( _V  \  1o ) )  e.  Fin }  |->  [_OrdIso (  _E  ,  ( `' f " ( _V 
\  1o ) ) )  /  h ]_ (seq𝜔 ( ( k  e. 
_V ,  z  e. 
_V  |->  ( ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )  +o  z ) ) ,  (/) ) `  dom  h
) ) )
Colors of variables: wff set class
This definition is referenced by:  cantnffval  7364
  Copyright terms: Public domain W3C validator