Metamath Proof Explorer

Theorem om2

Description: Two ways to double an ordinal. (Contributed by RP, 3-Jan-2025)

Ref Expression
Assertion om2 ⊢ A ∈ On → A + 𝑜 A = A ⋅ 𝑜 2 𝑜

Proof

Step Hyp Ref Expression
1 df-2o ⊢ 2 𝑜 = suc ⁡ 1 𝑜
2 1 oveq2i ⊢ A ⋅ 𝑜 2 𝑜 = A ⋅ 𝑜 suc ⁡ 1 𝑜
3 1on ⊢ 1 𝑜 ∈ On
4 omsuc ⊢ A ∈ On ∧ 1 𝑜 ∈ On → A ⋅ 𝑜 suc ⁡ 1 𝑜 = A ⋅ 𝑜 1 𝑜 + 𝑜 A
5 3 4 mpan2 ⊢ A ∈ On → A ⋅ 𝑜 suc ⁡ 1 𝑜 = A ⋅ 𝑜 1 𝑜 + 𝑜 A
6 om1 ⊢ A ∈ On → A ⋅ 𝑜 1 𝑜 = A
7 6 oveq1d ⊢ A ∈ On → A ⋅ 𝑜 1 𝑜 + 𝑜 A = A + 𝑜 A
8 5 7 eqtrd ⊢ A ∈ On → A ⋅ 𝑜 suc ⁡ 1 𝑜 = A + 𝑜 A
9 2 8 eqtr2id ⊢ A ∈ On → A + 𝑜 A = A ⋅ 𝑜 2 𝑜