Definition df-oexp 8486

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 8479	. 2 class ↑o
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		con0 6362	. . 3 class On
5	2	cv 1568	. . . . 5 class 𝑥
6		c0 4278	. . . . 5 class ∅
7	5, 6	wceq 1569	. . . 4 wff 𝑥 = ∅
8		c1o 8473	. . . . 5 class 1o
9	3	cv 1568	. . . . 5 class 𝑦
10	8, 9	cdif 4045	. . . 4 class (1o ∖ 𝑦)
11		vz	. . . . . . 7 setvar 𝑧
12		cvv 3450	. . . . . . 7 class V
13	11	cv 1568	. . . . . . . 8 class 𝑧
14		comu 8478	. . . . . . . 8 class ·o
15	13, 5, 14	co 7421	. . . . . . 7 class (𝑧 ·o 𝑥)
16	11, 12, 15	cmpt 5185	. . . . . 6 class (𝑧 ∈ V ↦ (𝑧 ·o 𝑥))
17	16, 8	crdg 8421	. . . . 5 class rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)
18	9, 17	cfv 6539	. . . 4 class (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)
19	7, 10, 18	cif 4481	. . 3 class if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))
20	2, 3, 4, 4, 19	cmpo 7423	. 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)))
21	1, 20	wceq 1569	1 wff ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)))

This definition is used by:  fnoe  8522  oev  8526