Definition df-oexp 8111

Description: Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.)

Assertion

Ref	Expression
df-oexp	⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)))

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-oexp

Step	Hyp	Ref	Expression
1		coe 8104	. 2 class ↑o
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		con0 6194	. . 3 class On
5	2	cv 1535	. . . . 5 class 𝑥
6		c0 4294	. . . . 5 class ∅
7	5, 6	wceq 1536	. . . 4 wff 𝑥 = ∅
8		c1o 8098	. . . . 5 class 1o
9	3	cv 1535	. . . . 5 class 𝑦
10	8, 9	cdif 3936	. . . 4 class (1o ∖ 𝑦)
11		vz	. . . . . . 7 setvar 𝑧
12		cvv 3497	. . . . . . 7 class V
13	11	cv 1535	. . . . . . . 8 class 𝑧
14		comu 8103	. . . . . . . 8 class ·o
15	13, 5, 14	co 7159	. . . . . . 7 class (𝑧 ·o 𝑥)
16	11, 12, 15	cmpt 5149	. . . . . 6 class (𝑧 ∈ V ↦ (𝑧 ·o 𝑥))
17	16, 8	crdg 8048	. . . . 5 class rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)
18	9, 17	cfv 6358	. . . 4 class (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)
19	7, 10, 18	cif 4470	. . 3 class if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))
20	2, 3, 4, 4, 19	cmpo 7161	. 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)))
21	1, 20	wceq 1536	1 wff ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)))

This definition is referenced by:  fnoe  8138  oev  8142