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

Definition df-oexp 7054
Description: Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.)
Assertion
Ref Expression
df-oexp  |-  ^o  =  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y
) ,  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
) ) )
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-oexp
StepHypRef Expression
1 coe 7047 . 2  class  ^o
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 con0 4792 . . 3  class  On
52cv 1398 . . . . 5  class  x
6 c0 3711 . . . . 5  class  (/)
75, 6wceq 1399 . . . 4  wff  x  =  (/)
8 c1o 7041 . . . . 5  class  1o
93cv 1398 . . . . 5  class  y
108, 9cdif 3386 . . . 4  class  ( 1o 
\  y )
11 vz . . . . . . 7  setvar  z
12 cvv 3034 . . . . . . 7  class  _V
1311cv 1398 . . . . . . . 8  class  z
14 comu 7046 . . . . . . . 8  class  .o
1513, 5, 14co 6196 . . . . . . 7  class  ( z  .o  x )
1611, 12, 15cmpt 4425 . . . . . 6  class  ( z  e.  _V  |->  ( z  .o  x ) )
1716, 8crdg 6993 . . . . 5  class  rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o )
189, 17cfv 5496 . . . 4  class  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
)
197, 10, 18cif 3857 . . 3  class  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
)
202, 3, 4, 4, 19cmpt2 6198 . 2  class  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
211, 20wceq 1399 1  wff  ^o  =  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y
) ,  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
) ) )
Colors of variables: wff setvar class
This definition is referenced by:  fnoe  7078  oev  7082
  Copyright terms: Public domain W3C validator