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

Definition df-oexp 6485
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 6478 . 2  class  ^o
2 vx . . 3  set  x
3 vy . . 3  set  y
4 con0 4392 . . 3  class  On
52cv 1622 . . . . 5  class  x
6 c0 3455 . . . . 5  class  (/)
75, 6wceq 1623 . . . 4  wff  x  =  (/)
8 c1o 6472 . . . . 5  class  1o
93cv 1622 . . . . 5  class  y
108, 9cdif 3149 . . . 4  class  ( 1o 
\  y )
11 vz . . . . . . 7  set  z
12 cvv 2788 . . . . . . 7  class  _V
1311cv 1622 . . . . . . . 8  class  z
14 comu 6477 . . . . . . . 8  class  .o
1513, 5, 14co 5858 . . . . . . 7  class  ( z  .o  x )
1611, 12, 15cmpt 4077 . . . . . 6  class  ( z  e.  _V  |->  ( z  .o  x ) )
1716, 8crdg 6422 . . . . 5  class  rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o )
189, 17cfv 5255 . . . 4  class  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
)
197, 10, 18cif 3565 . . 3  class  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
)
202, 3, 4, 4, 19cmpt2 5860 . 2  class  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
211, 20wceq 1623 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  6509  oev  6513
  Copyright terms: Public domain W3C validator