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