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

Definition df-cnf 7880
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 7915 of this function in terms of df-oi 7736. (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
StepHypRef Expression
1 ccnf 7879 . 2  class CNF
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 con0 4731 . . 3  class  On
5 vf . . . 4  setvar  f
6 vg . . . . . . 7  setvar  g
76cv 1368 . . . . . 6  class  g
8 c0 3649 . . . . . 6  class  (/)
9 cfsupp 7632 . . . . . 6  class finSupp
107, 8, 9wbr 4304 . . . . 5  wff  g finSupp  (/)
112cv 1368 . . . . . 6  class  x
123cv 1368 . . . . . 6  class  y
13 cmap 7226 . . . . . 6  class  ^m
1411, 12, 13co 6103 . . . . 5  class  ( x  ^m  y )
1510, 6, 14crab 2731 . . . 4  class  { g  e.  ( x  ^m  y )  |  g finSupp  (/)
}
16 vh . . . . 5  setvar  h
175cv 1368 . . . . . . 7  class  f
18 csupp 6702 . . . . . . 7  class supp
1917, 8, 18co 6103 . . . . . 6  class  ( f supp  (/) )
20 cep 4642 . . . . . 6  class  _E
2119, 20coi 7735 . . . . 5  class OrdIso (  _E  ,  ( f supp  (/) ) )
2216cv 1368 . . . . . . 7  class  h
2322cdm 4852 . . . . . 6  class  dom  h
24 vk . . . . . . . 8  setvar  k
25 vz . . . . . . . 8  setvar  z
26 cvv 2984 . . . . . . . 8  class  _V
2724cv 1368 . . . . . . . . . . . 12  class  k
2827, 22cfv 5430 . . . . . . . . . . 11  class  ( h `
 k )
29 coe 6931 . . . . . . . . . . 11  class  ^o
3011, 28, 29co 6103 . . . . . . . . . 10  class  ( x  ^o  ( h `  k ) )
3128, 17cfv 5430 . . . . . . . . . 10  class  ( f `
 ( h `  k ) )
32 comu 6930 . . . . . . . . . 10  class  .o
3330, 31, 32co 6103 . . . . . . . . 9  class  ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )
3425cv 1368 . . . . . . . . 9  class  z
35 coa 6929 . . . . . . . . 9  class  +o
3633, 34, 35co 6103 . . . . . . . 8  class  ( ( ( x  ^o  (
h `  k )
)  .o  ( f `
 ( h `  k ) ) )  +o  z )
3724, 25, 26, 26, 36cmpt2 6105 . . . . . . 7  class  ( k  e.  _V ,  z  e.  _V  |->  ( ( ( x  ^o  (
h `  k )
)  .o  ( f `
 ( h `  k ) ) )  +o  z ) )
3837, 8cseqom 6914 . . . . . 6  class seq𝜔 ( ( k  e. 
_V ,  z  e. 
_V  |->  ( ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )  +o  z ) ) ,  (/) )
3923, 38cfv 5430 . . . . 5  class  (seq𝜔 ( ( k  e.  _V , 
z  e.  _V  |->  ( ( ( x  ^o  ( h `  k
) )  .o  (
f `  ( h `  k ) ) )  +o  z ) ) ,  (/) ) `  dom  h )
4016, 21, 39csb 3300 . . . 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 )
415, 15, 40cmpt 4362 . . 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
) )
422, 3, 4, 4, 41cmpt2 6105 . 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
) ) )
431, 42wceq 1369 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 ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  cantnffval  7881
  Copyright terms: Public domain W3C validator