This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oe0

Description: Ordinal exponentiation with zero exponent. Definition 8.30 of TakeutiZaring p. 67. Definition 2.6 of Schloeder p. 4. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oe0 ⊢ A ∈ On → A ↑ 𝑜 ∅ = 1 𝑜

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = ∅ → A ↑ 𝑜 ∅ = ∅ ↑ 𝑜 ∅
2 oe0m0 ⊢ ∅ ↑ 𝑜 ∅ = 1 𝑜
3 1 2 eqtrdi ⊢ A = ∅ → A ↑ 𝑜 ∅ = 1 𝑜
4 3 adantl ⊢ A ∈ On ∧ A = ∅ → A ↑ 𝑜 ∅ = 1 𝑜
5 0elon ⊢ ∅ ∈ On
6 oevn0 ⊢ A ∈ On ∧ ∅ ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 ∅ = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ ∅
7 5 6 mpanl2 ⊢ A ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 ∅ = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ ∅
8 1oex ⊢ 1 𝑜 ∈ V
9 8 rdg0 ⊢ rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ ∅ = 1 𝑜
10 7 9 eqtrdi ⊢ A ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 ∅ = 1 𝑜
11 10 adantll ⊢ A ∈ On ∧ A ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 ∅ = 1 𝑜
12 4 11 oe0lem ⊢ A ∈ On ∧ A ∈ On → A ↑ 𝑜 ∅ = 1 𝑜
13 12 anidms ⊢ A ∈ On → A ↑ 𝑜 ∅ = 1 𝑜