Theorem nnssn0s

Description: The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	nnssn0s	$$⊢{\mathbb{N}}_s\subseteq {\mathbb{N}}_{\mathrm{0s}}$$

Proof

Step	Hyp	Ref	Expression
1		df-nns	$$⊢{\mathbb{N}}_s={\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}$$
2		difss	$$⊢{\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}\subseteq {\mathbb{N}}_{\mathrm{0s}}$$
3	1 2	eqsstri	$$⊢{\mathbb{N}}_s\subseteq {\mathbb{N}}_{\mathrm{0s}}$$