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	|- ( ( ( A e. On /\ A =/= (/) ) /\ C e. On ) -> ( B e. C -> ( A .o B ) e. ( A .o C ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. On /\ A =/= (/) ) -> A e. On )
2	1	anim1ci	|- ( ( ( A e. On /\ A =/= (/) ) /\ C e. On ) -> ( C e. On /\ A e. On ) )
3		on0eln0	|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
4	3	biimpar	|- ( ( A e. On /\ A =/= (/) ) -> (/) e. A )
5	4	adantr	|- ( ( ( A e. On /\ A =/= (/) ) /\ C e. On ) -> (/) e. A )
6		omordi	|- ( ( ( C e. On /\ A e. On ) /\ (/) e. A ) -> ( B e. C -> ( A .o B ) e. ( A .o C ) ) )
7	2 5 6	syl2anc	|- ( ( ( A e. On /\ A =/= (/) ) /\ C e. On ) -> ( B e. C -> ( A .o B ) e. ( A .o C ) ) )