Theorem oaordi3

Description: Ordinal addition of the same number on the left preserves the ordering of the numbers on the right. Lemma 3.6 of Schloeder p. 8. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	oaordi3	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( B e. C -> ( A +o B ) e. ( A +o C ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	|- ( ( A e. On /\ B e. On /\ C e. On ) -> C e. On )
2		simp1	|- ( ( A e. On /\ B e. On /\ C e. On ) -> A e. On )
3	1 2	jca	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( C e. On /\ A e. On ) )
4		oaordi	|- ( ( C e. On /\ A e. On ) -> ( B e. C -> ( A +o B ) e. ( A +o C ) ) )
5	3 4	syl	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( B e. C -> ( A +o B ) e. ( A +o C ) ) )