Theorem oaltublim

Description: Given C is a limit ordinal, the sum of any ordinal with an ordinal less than C is less than the sum of the first ordinal with C . Lemma 3.5 of Schloeder p. 7. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	oaltublim	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐶 ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		limord	⊢ ( Lim 𝐶 → Ord 𝐶 )
2		elex	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ V )
3	1 2	anim12i	⊢ ( ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) → ( Ord 𝐶 ∧ 𝐶 ∈ V ) )
4		elon2	⊢ ( 𝐶 ∈ On ↔ ( Ord 𝐶 ∧ 𝐶 ∈ V ) )
5	3 4	sylibr	⊢ ( ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ On )
6	5	3ad2ant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐶 ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ On )
7		simp1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐶 ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ On )
8	6 7	jca	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐶 ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) )
9		simp2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐶 ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝐶 )
10		oaordi	⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o 𝐶 ) ) )
11	8 9 10	sylc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐶 ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o 𝐶 ) )