Metamath Proof Explorer

Theorem omord2com

Description: When the same non-zero ordinal is multiplied on the left, ordering of the products is equivalent to the ordering of the ordinals on the right. Theorem 3.16 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion omord2com ⊢A∈On∧B∈On∧C∈On→B∈C∧∅∈A↔A⋅𝑜B∈A⋅𝑜C

Proof

Step Hyp Ref Expression
1 omord ⊢B∈On∧C∈On∧A∈On→B∈C∧∅∈A↔A⋅𝑜B∈A⋅𝑜C
2 1 3comr ⊢A∈On∧B∈On∧C∈On→B∈C∧∅∈A↔A⋅𝑜B∈A⋅𝑜C