Metamath Proof Explorer

Definition df-oexp

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

Ref Expression
Assertion df-oexp ⊢ ↑ 𝑜 = x ∈ On , y ∈ On ⟼ if x = ∅ 1 𝑜 ∖ y rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜 ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 coe class ↑ 𝑜
1 vx setvar x
2 con0 class On
3 vy setvar y
4 1 cv setvar x
5 c0 class ∅
6 4 5 wceq wff x = ∅
7 c1o class 1 𝑜
8 3 cv setvar y
9 7 8 cdif class 1 𝑜 ∖ y
10 vz setvar z
11 cvv class V
12 10 cv setvar z
13 comu class ⋅ 𝑜
14 12 4 13 co class z ⋅ 𝑜 x
15 10 11 14 cmpt class z ∈ V ⟼ z ⋅ 𝑜 x
16 15 7 crdg class rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜
17 8 16 cfv class rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜 ⁡ y
18 6 9 17 cif class if x = ∅ 1 𝑜 ∖ y rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜 ⁡ y
19 1 3 2 2 18 cmpo class x ∈ On , y ∈ On ⟼ if x = ∅ 1 𝑜 ∖ y rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜 ⁡ y
20 0 19 wceq wff ↑ 𝑜 = x ∈ On , y ∈ On ⟼ if x = ∅ 1 𝑜 ∖ y rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜 ⁡ y