Metamath Proof Explorer

Theorem naddword1

Description: Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 21-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 naddrid ⊢ A ∈ On → A + ∅ = A
2 1 adantr ⊢ A ∈ On ∧ B ∈ On → A + ∅ = A
3 0ss ⊢ ∅ ⊆ B
4 0elon ⊢ ∅ ∈ On
5 naddss2 ⊢ ∅ ∈ On ∧ B ∈ On ∧ A ∈ On → ∅ ⊆ B ↔ A + ∅ ⊆ A + B
6 4 5 mp3an1 ⊢ B ∈ On ∧ A ∈ On → ∅ ⊆ B ↔ A + ∅ ⊆ A + B
7 6 ancoms ⊢ 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