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

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐶 ∈ On )
2		simp1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐴 ∈ On )
3	1 2	jca	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) )
4		oaordi	⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o 𝐶 ) ) )
5	3 4	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o 𝐶 ) ) )