Theorem elnns2

Description: A positive surreal integer is a non-negative surreal integer greater than zero. (Contributed by Scott Fenton, 15-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		elnns	$$⊢A\in {\mathbb{N}}_s\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)$$
2		nesym	$$⊢A\ne 0_s\leftrightarrow \neg 0_s=A$$
3		n0sge0	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}A$$
4		0sno	$$⊢0_s\in \mathrm{No}$$
5		n0sno	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in \mathrm{No}$$
6		sleloe	$$⊢\left(0_s\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to \left(0_s{\le }_{s}A\leftrightarrow \left(0_s{<}_{s}A\vee 0_s=A\right)\right)$$
7	4 5 6	sylancr	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(0_s{\le }_{s}A\leftrightarrow \left(0_s{<}_{s}A\vee 0_s=A\right)\right)$$
8	3 7	mpbid	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(0_s{<}_{s}A\vee 0_s=A\right)$$
9	8	orcomd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(0_s=A\vee 0_s{<}_{s}A\right)$$
10	9	ord	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\neg 0_s=A\to 0_s{<}_{s}A\right)$$
11	2 10	biimtrid	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A\ne 0_s\to 0_s{<}_{s}A\right)$$
12		sgt0ne0	$$⊢0_s{<}_{s}A\to A\ne 0_s$$
13	11 12	impbid1	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A\ne 0_s\leftrightarrow 0_s{<}_{s}A\right)$$
14	13	pm5.32i	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{<}_{s}A\right)$$
15	1 14	bitri	$$⊢A\in {\mathbb{N}}_s\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{<}_{s}A\right)$$