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		0slt1s	$$⊢0_s{<}_s{1}_s$$
3		sgt0ne0	$$⊢0_s{<}_s{1}_s\to 1_s\ne 0_s$$
4	2 3	ax-mp	$$⊢1_s\ne 0_s$$
5		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)$$
6	1 4 5	mpbir2an	$$⊢1_s\in \left({\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}\right)$$
7		df-nns	$$⊢{\mathbb{N}}_s={\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}$$
8	6 7	eleqtrri	$$⊢1_s\in {\mathbb{N}}_s$$