Metamath Proof Explorer

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 ⊢A∈On∧B∈C∧Lim⁡C∧C∈V→A+𝑜B∈A+𝑜C

Proof

Step Hyp Ref Expression
1 limord ⊢Lim⁡C→Ord⁡C
2 elex ⊢C∈V→C∈V
3 1 2 anim12i ⊢Lim⁡C∧C∈V→Ord⁡C∧C∈V
4 elon2 ⊢C∈On↔Ord⁡C∧C∈V
5 3 4 sylibr ⊢Lim⁡C∧C∈V→C∈On
6 5 3ad2ant3 ⊢A∈On∧B∈C∧Lim⁡C∧C∈V→C∈On
7 simp1 ⊢A∈On∧B∈C∧Lim⁡C∧C∈V→A∈On
8 6 7 jca ⊢A∈On∧B∈C∧Lim⁡C∧C∈V→C∈On∧A∈On
9 simp2 ⊢A∈On∧B∈C∧Lim⁡C∧C∈V→B∈C
10 oaordi ⊢C∈On∧A∈On→B∈C→A+𝑜B∈A+𝑜C
11 8 9 10 sylc ⊢A∈On∧B∈C∧Lim⁡C∧C∈V→A+𝑜B∈A+𝑜C