Metamath Proof Explorer

Theorem oe2

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

Ref Expression
Assertion oe2 ⊢ 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 oesuc ⊢ A ∈ On ∧ 1 𝑜 ∈ On → A ↑ 𝑜 suc ⁡ 1 𝑜 = A ↑ 𝑜 1 𝑜 ⋅ 𝑜 A
5 3 4 mpan2 ⊢ A ∈ On → A ↑ 𝑜 suc ⁡ 1 𝑜 = A ↑ 𝑜 1 𝑜 ⋅ 𝑜 A
6 oe1 ⊢ 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 𝑜