Metamath Proof Explorer

Theorem oev

Description: Value of ordinal exponentiation. (Contributed by NM, 30-Dec-2004) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion oev ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 B = if A = ∅ 1 𝑜 ∖ B rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ y = A → y = ∅ ↔ A = ∅
2 oveq2 ⊢ y = A → x ⋅ 𝑜 y = x ⋅ 𝑜 A
3 2 mpteq2dv ⊢ y = A → x ∈ V ⟼ x ⋅ 𝑜 y = x ∈ V ⟼ x ⋅ 𝑜 A
4 rdgeq1 ⊢ x ∈ V ⟼ x ⋅ 𝑜 y = x ∈ V ⟼ x ⋅ 𝑜 A → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 y 1 𝑜 = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜
5 3 4 syl ⊢ y = A → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 y 1 𝑜 = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜
6 5 fveq1d ⊢ y = A → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 y 1 𝑜 ⁡ z = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ z
7 1 6 ifbieq2d ⊢ y = A → if y = ∅ 1 𝑜 ∖ z rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 y 1 𝑜 ⁡ z = if A = ∅ 1 𝑜 ∖ z rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ z
8 difeq2 ⊢ z = B → 1 𝑜 ∖ z = 1 𝑜 ∖ B
9 fveq2 ⊢ z = B → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ z = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
10 8 9 ifeq12d ⊢ z = B → if A = ∅ 1 𝑜 ∖ z rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ z = if A = ∅ 1 𝑜 ∖ B rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
11 df-oexp ⊢ ↑ 𝑜 = y ∈ On , z ∈ On ⟼ if y = ∅ 1 𝑜 ∖ z rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 y 1 𝑜 ⁡ z
12 1oex ⊢ 1 𝑜 ∈ V
13 12 difexi ⊢ 1 𝑜 ∖ B ∈ V
14 fvex ⊢ rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B ∈ V
15 13 14 ifex ⊢ if A = ∅ 1 𝑜 ∖ B rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B ∈ V
16 7 10 11 15 ovmpo ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 B = if A = ∅ 1 𝑜 ∖ B rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B