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	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐴 ⊆ ( 𝐴 +o 𝐵 ) )

Proof

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