Metamath Proof Explorer

Theorem oe1

Description: Ordinal exponentiation with an exponent of 1. Lemma 2.16 of Schloeder p. 6. (Contributed by NM, 2-Jan-2005)

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

Proof

Step Hyp Ref Expression
1 df-1o ⊢ 1 𝑜 = suc ⁡ ∅
2 1 oveq2i ⊢ A ↑ 𝑜 1 𝑜 = A ↑ 𝑜 suc ⁡ ∅
3 peano1 ⊢ ∅ ∈ ω
4 onesuc ⊢ A ∈ On ∧ ∅ ∈ ω → A ↑ 𝑜 suc ⁡ ∅ = A ↑ 𝑜 ∅ ⋅ 𝑜 A
5 3 4 mpan2 ⊢ A ∈ On → A ↑ 𝑜 suc ⁡ ∅ = A ↑ 𝑜 ∅ ⋅ 𝑜 A
6 2 5 eqtrid ⊢ A ∈ On → A ↑ 𝑜 1 𝑜 = A ↑ 𝑜 ∅ ⋅ 𝑜 A
7 oe0 ⊢ A ∈ On → A ↑ 𝑜 ∅ = 1 𝑜
8 7 oveq1d ⊢ A ∈ On → A ↑ 𝑜 ∅ ⋅ 𝑜 A = 1 𝑜 ⋅ 𝑜 A
9 om1r ⊢ A ∈ On → 1 𝑜 ⋅ 𝑜 A = A
10 6 8 9 3eqtrd ⊢ A ∈ On → A ↑ 𝑜 1 𝑜 = A