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

Definition df-oexp 6924
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 6917 . 2  class  ^o
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 con0 4717 . . 3  class  On
52cv 1368 . . . . 5  class  x
6 c0 3635 . . . . 5  class  (/)
75, 6wceq 1369 . . . 4  wff  x  =  (/)
8 c1o 6911 . . . . 5  class  1o
93cv 1368 . . . . 5  class  y
108, 9cdif 3323 . . . 4  class  ( 1o 
\  y )
11 vz . . . . . . 7  setvar  z
12 cvv 2970 . . . . . . 7  class  _V
1311cv 1368 . . . . . . . 8  class  z
14 comu 6916 . . . . . . . 8  class  .o
1513, 5, 14co 6089 . . . . . . 7  class  ( z  .o  x )
1611, 12, 15cmpt 4348 . . . . . 6  class  ( z  e.  _V  |->  ( z  .o  x ) )
1716, 8crdg 6863 . . . . 5  class  rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o )
189, 17cfv 5416 . . . 4  class  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
)
197, 10, 18cif 3789 . . 3  class  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
)
202, 3, 4, 4, 19cmpt2 6091 . 2  class  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
211, 20wceq 1369 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  6948  oev  6952
  Copyright terms: Public domain W3C validator