Metamath Proof Explorer

Theorem om1om1r

Description: Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of Schloeder p. 5. See om1 and om1r for individual statements. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion om1om1r ⊢ A ∈ On → 1 𝑜 ⋅ 𝑜 A = A ⋅ 𝑜 1 𝑜 ∧ A ⋅ 𝑜 1 𝑜 = A

Proof

Step Hyp Ref Expression
1 om1r ⊢ A ∈ On → 1 𝑜 ⋅ 𝑜 A = A
2 om1 ⊢ A ∈ On → A ⋅ 𝑜 1 𝑜 = A
3 1 2 eqtr4d ⊢ A ∈ On → 1 𝑜 ⋅ 𝑜 A = A ⋅ 𝑜 1 𝑜
4 3 2 jca ⊢ A ∈ On → 1 𝑜 ⋅ 𝑜 A = A ⋅ 𝑜 1 𝑜 ∧ A ⋅ 𝑜 1 𝑜 = A