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

Definition df-oexp 6439
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 6432 . 2  class  ^o
2 vx . . 3  set  x
3 vy . . 3  set  y
4 con0 4350 . . 3  class  On
52cv 1618 . . . . 5  class  x
6 c0 3416 . . . . 5  class  (/)
75, 6wceq 1619 . . . 4  wff  x  =  (/)
8 c1o 6426 . . . . 5  class  1o
93cv 1618 . . . . 5  class  y
108, 9cdif 3110 . . . 4  class  ( 1o 
\  y )
11 vz . . . . . . 7  set  z
12 cvv 2757 . . . . . . 7  class  _V
1311cv 1618 . . . . . . . 8  class  z
14 comu 6431 . . . . . . . 8  class  .o
1513, 5, 14co 5778 . . . . . . 7  class  ( z  .o  x )
1611, 12, 15cmpt 4037 . . . . . 6  class  ( z  e.  _V  |->  ( z  .o  x ) )
1716, 8crdg 6376 . . . . 5  class  rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o )
189, 17cfv 4659 . . . 4  class  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
)
197, 10, 18cif 3525 . . 3  class  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
)
202, 3, 4, 4, 19cmpt2 5780 . 2  class  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
211, 20wceq 1619 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 set class
This definition is referenced by:  fnoe  6463  oev  6467
  Copyright terms: Public domain W3C validator