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

Definition df-oexp 7126
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 7119 . 2  class  ^o
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 con0 4871 . . 3  class  On
52cv 1373 . . . . 5  class  x
6 c0 3778 . . . . 5  class  (/)
75, 6wceq 1374 . . . 4  wff  x  =  (/)
8 c1o 7113 . . . . 5  class  1o
93cv 1373 . . . . 5  class  y
108, 9cdif 3466 . . . 4  class  ( 1o 
\  y )
11 vz . . . . . . 7  setvar  z
12 cvv 3106 . . . . . . 7  class  _V
1311cv 1373 . . . . . . . 8  class  z
14 comu 7118 . . . . . . . 8  class  .o
1513, 5, 14co 6275 . . . . . . 7  class  ( z  .o  x )
1611, 12, 15cmpt 4498 . . . . . 6  class  ( z  e.  _V  |->  ( z  .o  x ) )
1716, 8crdg 7065 . . . . 5  class  rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o )
189, 17cfv 5579 . . . 4  class  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
)
197, 10, 18cif 3932 . . 3  class  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
)
202, 3, 4, 4, 19cmpt2 6277 . 2  class  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
211, 20wceq 1374 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  7150  oev  7154
  Copyright terms: Public domain W3C validator