Theorem n0s0m1

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

	Ref	Expression
Assertion	n0s0m1	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A=0_s\vee A{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢x=0_s\to \left(x=0_s\leftrightarrow 0_s=0_s\right)$$
2		oveq1	$$⊢x=0_s\to x{-}_s{1}_s=0_s{-}_s{1}_s$$
3	2	eleq1d	$$⊢x=0_s\to \left(x{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow 0_s{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
4	1 3	orbi12d	$$⊢x=0_s\to \left(\left(x=0_s\vee x{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(0_s=0_s\vee 0_s{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
5		eqeq1	$$⊢x=y\to \left(x=0_s\leftrightarrow y=0_s\right)$$
6		oveq1	$$⊢x=y\to x{-}_s{1}_s=y{-}_s{1}_s$$
7	6	eleq1d	$$⊢x=y\to \left(x{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow y{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
8	5 7	orbi12d	$$⊢x=y\to \left(\left(x=0_s\vee x{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(y=0_s\vee y{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
9		eqeq1	$$⊢x=y{+}_s{1}_s\to \left(x=0_s\leftrightarrow y{+}_s{1}_s=0_s\right)$$
10		oveq1	$$⊢x=y{+}_s{1}_s\to x{-}_s{1}_s=\left(y{+}_s{1}_s\right){-}_s{1}_s$$
11	10	eleq1d	$$⊢x=y{+}_s{1}_s\to \left(x{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
12	9 11	orbi12d	$$⊢x=y{+}_s{1}_s\to \left(\left(x=0_s\vee x{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(y{+}_s{1}_s=0_s\vee \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
13		eqeq1	$$⊢x=A\to \left(x=0_s\leftrightarrow A=0_s\right)$$
14		oveq1	$$⊢x=A\to x{-}_s{1}_s=A{-}_s{1}_s$$
15	14	eleq1d	$$⊢x=A\to \left(x{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
16	13 15	orbi12d	$$⊢x=A\to \left(\left(x=0_s\vee x{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A=0_s\vee A{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
17		eqid	$$⊢0_s=0_s$$
18	17	orci	$$⊢\left(0_s=0_s\vee 0_s{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
19		n0no	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y\in \mathrm{No}$$
20		1no	$$⊢1_s\in \mathrm{No}$$
21		pncans	$$⊢\left(y\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(y{+}_s{1}_s\right){-}_s{1}_s=y$$
22	19 20 21	sylancl	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(y{+}_s{1}_s\right){-}_s{1}_s=y$$
23		id	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y\in {\mathbb{N}}_{\mathrm{0s}}$$
24	22 23	eqeltrd	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
25	24	olcd	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(y{+}_s{1}_s=0_s\vee \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
26	25	a1d	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\left(y=0_s\vee y{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(y{+}_s{1}_s=0_s\vee \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
27	4 8 12 16 18 26	n0sind	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A=0_s\vee A{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$