![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-oexpi | Unicode version |
Description: Define the ordinal
exponentiation operation.
This definition is similar to a conventional definition of
exponentiation except that it defines 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 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coei 6430 |
. 2
![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | con0 4375 |
. . 3
![]() ![]() | |
5 | 3 | cv 1362 |
. . . 4
![]() ![]() |
6 | vz |
. . . . . 6
![]() ![]() | |
7 | cvv 2749 |
. . . . . 6
![]() ![]() | |
8 | 6 | cv 1362 |
. . . . . . 7
![]() ![]() |
9 | 2 | cv 1362 |
. . . . . . 7
![]() ![]() |
10 | comu 6429 |
. . . . . . 7
![]() ![]() | |
11 | 8, 9, 10 | co 5888 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() |
12 | 6, 7, 11 | cmpt 4076 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | c1o 6424 |
. . . . 5
![]() ![]() | |
14 | 12, 13 | crdg 6384 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 5, 14 | cfv 5228 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 2, 3, 4, 4, 15 | cmpo 5890 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 1, 16 | wceq 1363 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: fnoei 6467 oeiexg 6468 oeiv 6471 |
Copyright terms: Public domain | W3C validator |