Definition df-oexp 7453

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

Assertion

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

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-oexp

Step	Hyp	Ref	Expression
1		coe 7446	. 2 class ↑𝑜
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		con0 5640	. . 3 class On
5	2	cv 1474	. . . . 5 class 𝑥
6		c0 3874	. . . . 5 class ∅
7	5, 6	wceq 1475	. . . 4 wff 𝑥 = ∅
8		c1o 7440	. . . . 5 class 1𝑜
9	3	cv 1474	. . . . 5 class 𝑦
10	8, 9	cdif 3537	. . . 4 class (1𝑜 ∖ 𝑦)
11		vz	. . . . . . 7 setvar 𝑧
12		cvv 3173	. . . . . . 7 class V
13	11	cv 1474	. . . . . . . 8 class 𝑧
14		comu 7445	. . . . . . . 8 class ·𝑜
15	13, 5, 14	co 6549	. . . . . . 7 class (𝑧 ·𝑜 𝑥)
16	11, 12, 15	cmpt 4643	. . . . . 6 class (𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥))
17	16, 8	crdg 7392	. . . . 5 class rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)
18	9, 17	cfv 5804	. . . 4 class (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦)
19	7, 10, 18	cif 4036	. . 3 class if(𝑥 = ∅, (1𝑜 ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦))
20	2, 3, 4, 4, 19	cmpt2 6551	. 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1𝑜 ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦)))
21	1, 20	wceq 1475	1 wff ↑𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1𝑜 ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦)))

This definition is referenced by:  fnoe  7477  oev  7481