Theorem omord2i

Description: Ordinal multiplication of the same non-zero number on the left preserves the ordering of the numbers on the right. Lemma 3.15 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	omord2i	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ On )
2	1	anim1ci	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ 𝐶 ∈ On ) → ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) )
3		on0eln0	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
4	3	biimpar	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) → ∅ ∈ 𝐴 )
5	4	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ 𝐶 ∈ On ) → ∅ ∈ 𝐴 )
6		omordi	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )
7	2 5 6	syl2anc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )