ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-oexpi Unicode version

Definition df-oexpi 6401
Description: Define the ordinal exponentiation operation.

This definition is similar to a conventional definition of exponentiation except that it defines  (/)o  A to be  1o for all  A  e.  On, in order to avoid having different cases for whether the base is  (/) or not. (Contributed by Mario Carneiro, 4-Jul-2019.)

Assertion
Ref Expression
df-oexpi  |-o  =  ( x  e.  On ,  y  e.  On  |->  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
)
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-oexpi
StepHypRef Expression
1 coei 6394 . 2  classo
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 con0 4348 . . 3  class  On
53cv 1347 . . . 4  class  y
6 vz . . . . . 6  setvar  z
7 cvv 2730 . . . . . 6  class  _V
86cv 1347 . . . . . . 7  class  z
92cv 1347 . . . . . . 7  class  x
10 comu 6393 . . . . . . 7  class  .o
118, 9, 10co 5853 . . . . . 6  class  ( z  .o  x )
126, 7, 11cmpt 4050 . . . . 5  class  ( z  e.  _V  |->  ( z  .o  x ) )
13 c1o 6388 . . . . 5  class  1o
1412, 13crdg 6348 . . . 4  class  rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o )
155, 14cfv 5198 . . 3  class  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
)
162, 3, 4, 4, 15cmpo 5855 . 2  class  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
) )
171, 16wceq 1348 1  wffo  =  ( x  e.  On ,  y  e.  On  |->  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
)
Colors of variables: wff set class
This definition is referenced by:  fnoei  6431  oeiexg  6432  oeiv  6435
  Copyright terms: Public domain W3C validator