Metamath Proof Explorer

Theorem oevn0

Description: Value of ordinal exponentiation at a nonzero base. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 on0eln0 ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅
2 df-ne ⊢ A ≠ ∅ ↔ ¬ A = ∅
3 1 2 bitrdi ⊢ A ∈ On → ∅ ∈ A ↔ ¬ A = ∅
4 3 adantr ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ A ↔ ¬ A = ∅
5 oev ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 B = if A = ∅ 1 𝑜 ∖ B rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
6 iffalse ⊢ ¬ A = ∅ → if A = ∅ 1 𝑜 ∖ B rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
7 5 6 sylan9eq ⊢ A ∈ On ∧ B ∈ On ∧ ¬ A = ∅ → A ↑ 𝑜 B = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
8 7 ex ⊢ A ∈ On ∧ B ∈ On → ¬ A = ∅ → A ↑ 𝑜 B = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
9 4 8 sylbid ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ A → A ↑ 𝑜 B = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
10 9 imp ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 B = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B