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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ↔ ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		omord	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ↔ ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )
2	1	3comr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ↔ ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )