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

Definition df-oexpi 6422
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.

We do not yet have an extensive development of ordinal exponentiation. For background on ordinal exponentiation without excluded middle, see Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu (2025), "Ordinal Exponentiation in Homotopy Type Theory", arXiv:2501.14542 , https://arxiv.org/abs/2501.14542 which is formalized in the TypeTopology proof library at https://ordinal-exponentiation-hott.github.io/.

(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 6415 . 2  classo
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 con0 4363 . . 3  class  On
53cv 1352 . . . 4  class  y
6 vz . . . . . 6  setvar  z
7 cvv 2737 . . . . . 6  class  _V
86cv 1352 . . . . . . 7  class  z
92cv 1352 . . . . . . 7  class  x
10 comu 6414 . . . . . . 7  class  .o
118, 9, 10co 5874 . . . . . 6  class  ( z  .o  x )
126, 7, 11cmpt 4064 . . . . 5  class  ( z  e.  _V  |->  ( z  .o  x ) )
13 c1o 6409 . . . . 5  class  1o
1412, 13crdg 6369 . . . 4  class  rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o )
155, 14cfv 5216 . . 3  class  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
)
162, 3, 4, 4, 15cmpo 5876 . 2  class  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  .o  x ) ) ,  1o ) `  y
) )
171, 16wceq 1353 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  6452  oeiexg  6453  oeiv  6456
  Copyright terms: Public domain W3C validator