Theorem 1nns

Description: Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	1nns	$$⊢1_s\in {\mathbb{N}}_s$$

Proof

Step	Hyp	Ref	Expression
1		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
2		1ne0s	$$⊢1_s\ne 0_s$$
3		eldifsn	$$⊢1_s\in \left({\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}\right)\leftrightarrow \left(1_s\in {\mathbb{N}}_{\mathrm{0s}}\wedge 1_s\ne 0_s\right)$$
4	1 2 3	mpbir2an	$$⊢1_s\in \left({\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}\right)$$
5		df-nns	$$⊢{\mathbb{N}}_s={\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}$$
6	4 5	eleqtrri	$$⊢1_s\in {\mathbb{N}}_s$$