Theorem elnns

Description: Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	elnns	$$⊢A\in {\mathbb{N}}_s\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-nns	$$⊢{\mathbb{N}}_s={\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}$$
2	1	eleq2i	$$⊢A\in {\mathbb{N}}_s\leftrightarrow A\in \left({\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}\right)$$
3		eldifsn	$$⊢A\in \left({\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)$$
4	2 3	bitri	$$⊢A\in {\mathbb{N}}_s\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)$$