Definition df-oexpi 6489

Description: Define the ordinal exponentiation operation.

This definition is similar to a conventional definition of exponentiation except that it defines ∅ ↑_o 𝐴 to be 1_o 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

Step	Hyp	Ref	Expression
1		coei 6482	. 2 class ↑o
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		con0 4399	. . 3 class On
5	3	cv 1363	. . . 4 class 𝑦
6		vz	. . . . . 6 setvar 𝑧
7		cvv 2763	. . . . . 6 class V
8	6	cv 1363	. . . . . . 7 class 𝑧
9	2	cv 1363	. . . . . . 7 class 𝑥
10		comu 6481	. . . . . . 7 class ·o
11	8, 9, 10	co 5925	. . . . . 6 class (𝑧 ·o 𝑥)
12	6, 7, 11	cmpt 4095	. . . . 5 class (𝑧 ∈ V ↦ (𝑧 ·o 𝑥))
13		c1o 6476	. . . . 5 class 1o
14	12, 13	crdg 6436	. . . 4 class rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)
15	5, 14	cfv 5259	. . 3 class (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)
16	2, 3, 4, 4, 15	cmpo 5927	. 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))
17	1, 16	wceq 1364	1 wff ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))

This definition is referenced by:  fnoei  6519  oeiexg  6520  oeiv  6523