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

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

This definition is similar to a conventional definition of exponentiation except that it defines โˆ… โ†‘o ๐ด to be 1o for all ๐ด โˆˆ 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 = (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ))
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐‘ง

Detailed syntax breakdown of Definition df-oexpi
StepHypRef Expression
1 coei 6416 . 2 class โ†‘o
2 vx . . 3 setvar ๐‘ฅ
3 vy . . 3 setvar ๐‘ฆ
4 con0 4364 . . 3 class On
53cv 1352 . . . 4 class ๐‘ฆ
6 vz . . . . . 6 setvar ๐‘ง
7 cvv 2738 . . . . . 6 class V
86cv 1352 . . . . . . 7 class ๐‘ง
92cv 1352 . . . . . . 7 class ๐‘ฅ
10 comu 6415 . . . . . . 7 class ยทo
118, 9, 10co 5875 . . . . . 6 class (๐‘ง ยทo ๐‘ฅ)
126, 7, 11cmpt 4065 . . . . 5 class (๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ))
13 c1o 6410 . . . . 5 class 1o
1412, 13crdg 6370 . . . 4 class rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)
155, 14cfv 5217 . . 3 class (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ)
162, 3, 4, 4, 15cmpo 5877 . 2 class (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ))
171, 16wceq 1353 1 wff โ†‘o = (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ (rec((๐‘ง โˆˆ V โ†ฆ (๐‘ง ยทo ๐‘ฅ)), 1o)โ€˜๐‘ฆ))
Colors of variables: wff set class
This definition is referenced by:  fnoei  6453  oeiexg  6454  oeiv  6457
  Copyright terms: Public domain W3C validator