Theorem eln0s

Description: A non-negative surreal integer is zero or a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	eln0s	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(A\in {\mathbb{N}}_s\vee A=0_s\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm2.1	$$⊢\left(\neg A=0_s\vee A=0_s\right)$$
2		df-ne	$$⊢A\ne 0_s\leftrightarrow \neg A=0_s$$
3	2	orbi1i	$$⊢\left(A\ne 0_s\vee A=0_s\right)\leftrightarrow \left(\neg A=0_s\vee A=0_s\right)$$
4	1 3	mpbir	$$⊢\left(A\ne 0_s\vee A=0_s\right)$$
5		ordir	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)\vee A=0_s\right)\leftrightarrow \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee A=0_s\right)\wedge \left(A\ne 0_s\vee A=0_s\right)\right)$$
6	4 5	mpbiran2	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)\vee A=0_s\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee A=0_s\right)$$
7		elnns	$$⊢A\in {\mathbb{N}}_s\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)$$
8	7	orbi1i	$$⊢\left(A\in {\mathbb{N}}_s\vee A=0_s\right)\leftrightarrow \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\ne 0_s\right)\vee A=0_s\right)$$
9		orc	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee A=0_s\right)$$
10		id	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in {\mathbb{N}}_{\mathrm{0s}}$$
11		id	$$⊢A=0_s\to A=0_s$$
12		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
13	11 12	eqeltrdi	$$⊢A=0_s\to A\in {\mathbb{N}}_{\mathrm{0s}}$$
14	10 13	jaoi	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee A=0_s\right)\to A\in {\mathbb{N}}_{\mathrm{0s}}$$
15	9 14	impbii	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee A=0_s\right)$$
16	6 8 15	3bitr4ri	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(A\in {\mathbb{N}}_s\vee A=0_s\right)$$