Metamath Proof Explorer

Theorem oaword1

Description: An ordinal is less than or equal to its sum with another. Part of Exercise 5 of TakeutiZaring p. 62. (For the other part see oaord1 .) (Contributed by NM, 6-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oa0 ⊢ A ∈ On → A + 𝑜 ∅ = A
2 1 adantr ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 ∅ = A
3 0ss ⊢ ∅ ⊆ B
4 0elon ⊢ ∅ ∈ On
5 oaword ⊢ ∅ ∈ On ∧ B ∈ On ∧ A ∈ On → ∅ ⊆ B ↔ A + 𝑜 ∅ ⊆ A + 𝑜 B
6 5 3com13 ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ On → ∅ ⊆ B ↔ A + 𝑜 ∅ ⊆ A + 𝑜 B
7 4 6 mp3an3 ⊢ A ∈ On ∧ B ∈ On → ∅ ⊆ B ↔ A + 𝑜 ∅ ⊆ A + 𝑜 B
8 3 7 mpbii ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 ∅ ⊆ A + 𝑜 B
9 2 8 eqsstrrd ⊢ A ∈ On ∧ B ∈ On → A ⊆ A + 𝑜 B