This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnaword2

Description: Weak ordering property of addition. (Contributed by NM, 9-Nov-2002)

		Ref	Expression
	Assertion	nnaword2	$⊢ (A \in ω \land B \in ω) \to A \subseteq B +_{𝑜} A$

Step	Hyp	Ref	Expression
1		nnaword1	$⊢ (A \in ω \land B \in ω) \to A \subseteq A +_{𝑜} B$
2		nnacom	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B = B +_{𝑜} A$
3	1 2	sseqtrd	$⊢ (A \in ω \land B \in ω) \to A \subseteq B +_{𝑜} A$