Metamath Proof Explorer

Theorem nnaword1

Description: Weak ordering property of addition. (Contributed by NM, 9-Nov-2002) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnaword1 ⊢ A ∈ ω ∧ B ∈ ω → A ⊆ A + 𝑜 B

Proof

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