![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-oexpi | GIF version |
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.) |
Ref | Expression |
---|---|
df-oexpi | ⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coei 6409 | . 2 class ↑o | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | con0 4359 | . . 3 class On | |
5 | 3 | cv 1352 | . . . 4 class 𝑦 |
6 | vz | . . . . . 6 setvar 𝑧 | |
7 | cvv 2737 | . . . . . 6 class V | |
8 | 6 | cv 1352 | . . . . . . 7 class 𝑧 |
9 | 2 | cv 1352 | . . . . . . 7 class 𝑥 |
10 | comu 6408 | . . . . . . 7 class ·o | |
11 | 8, 9, 10 | co 5868 | . . . . . 6 class (𝑧 ·o 𝑥) |
12 | 6, 7, 11 | cmpt 4061 | . . . . 5 class (𝑧 ∈ V ↦ (𝑧 ·o 𝑥)) |
13 | c1o 6403 | . . . . 5 class 1o | |
14 | 12, 13 | crdg 6363 | . . . 4 class rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o) |
15 | 5, 14 | cfv 5211 | . . 3 class (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦) |
16 | 2, 3, 4, 4, 15 | cmpo 5870 | . 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)) |
17 | 1, 16 | wceq 1353 | 1 wff ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)) |
Colors of variables: wff set class |
This definition is referenced by: fnoei 6446 oeiexg 6447 oeiv 6450 |
Copyright terms: Public domain | W3C validator |