Metamath Proof Explorer

Theorem oaword2

Description: An ordinal is less than or equal to its sum with another. Theorem 21 of Suppes p. 209. Lemma 3.3 of Schloeder p. 7. (Contributed by NM, 7-Dec-2004)

Ref Expression
Assertion oaword2 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B + 𝑜 A

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ B
2 0elon ⊢ ∅ ∈ On
3 oawordri ⊢ ∅ ∈ On ∧ B ∈ On ∧ A ∈ On → ∅ ⊆ B → ∅ + 𝑜 A ⊆ B + 𝑜 A
4 2 3 mp3an1 ⊢ B ∈ On ∧ A ∈ On → ∅ ⊆ B → ∅ + 𝑜 A ⊆ B + 𝑜 A
5 oa0r ⊢ A ∈ On → ∅ + 𝑜 A = A
6 5 adantl ⊢ B ∈ On ∧ A ∈ On → ∅ + 𝑜 A = A
7 6 sseq1d ⊢ B ∈ On ∧ A ∈ On → ∅ + 𝑜 A ⊆ B + 𝑜 A ↔ A ⊆ B + 𝑜 A
8 4 7 sylibd ⊢ B ∈ On ∧ A ∈ On → ∅ ⊆ B → A ⊆ B + 𝑜 A
9 1 8 mpi ⊢ B ∈ On ∧ A ∈ On → A ⊆ B + 𝑜 A
10 9 ancoms ⊢ A ∈ On ∧ B ∈ On → A ⊆ B + 𝑜 A