Theorem nnssno

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

	Ref	Expression
Assertion	nnssno	$$⊢{\mathbb{N}}_s\subseteq \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		nnssn0s	$$⊢{\mathbb{N}}_s\subseteq {\mathbb{N}}_{\mathrm{0s}}$$
2		n0ssno	$$⊢{\mathbb{N}}_{\mathrm{0s}}\subseteq \mathrm{No}$$
3	1 2	sstri	$$⊢{\mathbb{N}}_s\subseteq \mathrm{No}$$