Definition df-oexp 8468

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 8461	. 2 class ↑o
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		con0 6361	. . 3 class On
5	2	cv 1540	. . . . 5 class 𝑥
6		c0 4321	. . . . 5 class ∅
7	5, 6	wceq 1541	. . . 4 wff 𝑥 = ∅
8		c1o 8455	. . . . 5 class 1o
9	3	cv 1540	. . . . 5 class 𝑦
10	8, 9	cdif 3944	. . . 4 class (1o ∖ 𝑦)
11		vz	. . . . . . 7 setvar 𝑧
12		cvv 3474	. . . . . . 7 class V
13	11	cv 1540	. . . . . . . 8 class 𝑧
14		comu 8460	. . . . . . . 8 class ·o
15	13, 5, 14	co 7405	. . . . . . 7 class (𝑧 ·o 𝑥)
16	11, 12, 15	cmpt 5230	. . . . . 6 class (𝑧 ∈ V ↦ (𝑧 ·o 𝑥))
17	16, 8	crdg 8405	. . . . 5 class rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)
18	9, 17	cfv 6540	. . . 4 class (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)
19	7, 10, 18	cif 4527	. . 3 class if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))
20	2, 3, 4, 4, 19	cmpo 7407	. 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)))
21	1, 20	wceq 1541	1 wff ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)))

This definition is referenced by:  fnoe  8506  oev  8510