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

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

This definition is similar to a conventional definition of exponentiation except that it defines  (/)𝑜  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  |-𝑜  =  ( 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 6064 . 2  class𝑜
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 con0 4126 . . 3  class  On
53cv 1284 . . . 4  class  y
6 vz . . . . . 6  setvar  z
7 cvv 2602 . . . . . 6  class  _V
86cv 1284 . . . . . . 7  class  z
92cv 1284 . . . . . . 7  class  x
10 comu 6063 . . . . . . 7  class  .o
118, 9, 10co 5543 . . . . . 6  class  ( z  .o  x )
126, 7, 11cmpt 3847 . . . . 5  class  ( z  e.  _V  |->  ( z  .o  x ) )
13 c1o 6058 . . . . 5  class  1o
1412, 13crdg 6018 . . . 4  class  rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o )
155, 14cfv 4932 . . 3  class  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
)
162, 3, 4, 4, 15cmpt2 5545 . 2  class  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
) )
171, 16wceq 1285 1  wff𝑜  =  ( 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  6096  oeiexg  6097  oeiv  6100
  Copyright terms: Public domain W3C validator