Theorem n0s0suc

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

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

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢y=0_s\to \left(y=0_s\leftrightarrow 0_s=0_s\right)$$
2		eqeq1	$$⊢y=0_s\to \left(y=x{+}_s{1}_s\leftrightarrow 0_s=x{+}_s{1}_s\right)$$
3	2	rexbidv	$$⊢y=0_s\to \left(\exists x\in {\mathbb{N}}_{\mathrm{0s}}y=x{+}_s{1}_s\leftrightarrow \exists x\in {\mathbb{N}}_{\mathrm{0s}}{0}_s=x{+}_s{1}_s\right)$$
4	1 3	orbi12d	$$⊢y=0_s\to \left(\left(y=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}y=x{+}_s{1}_s\right)\leftrightarrow \left(0_s=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}{0}_s=x{+}_s{1}_s\right)\right)$$
5		eqeq1	$$⊢y=z\to \left(y=0_s\leftrightarrow z=0_s\right)$$
6		eqeq1	$$⊢y=z\to \left(y=x{+}_s{1}_s\leftrightarrow z=x{+}_s{1}_s\right)$$
7	6	rexbidv	$$⊢y=z\to \left(\exists x\in {\mathbb{N}}_{\mathrm{0s}}y=x{+}_s{1}_s\leftrightarrow \exists x\in {\mathbb{N}}_{\mathrm{0s}}z=x{+}_s{1}_s\right)$$
8	5 7	orbi12d	$$⊢y=z\to \left(\left(y=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}y=x{+}_s{1}_s\right)\leftrightarrow \left(z=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}z=x{+}_s{1}_s\right)\right)$$
9		eqeq1	$$⊢y=z{+}_s{1}_s\to \left(y=0_s\leftrightarrow z{+}_s{1}_s=0_s\right)$$
10		eqeq1	$$⊢y=z{+}_s{1}_s\to \left(y=x{+}_s{1}_s\leftrightarrow z{+}_s{1}_s=x{+}_s{1}_s\right)$$
11	10	rexbidv	$$⊢y=z{+}_s{1}_s\to \left(\exists x\in {\mathbb{N}}_{\mathrm{0s}}y=x{+}_s{1}_s\leftrightarrow \exists x\in {\mathbb{N}}_{\mathrm{0s}}z{+}_s{1}_s=x{+}_s{1}_s\right)$$
12	9 11	orbi12d	$$⊢y=z{+}_s{1}_s\to \left(\left(y=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}y=x{+}_s{1}_s\right)\leftrightarrow \left(z{+}_s{1}_s=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}z{+}_s{1}_s=x{+}_s{1}_s\right)\right)$$
13		eqeq1	$$⊢y=A\to \left(y=0_s\leftrightarrow A=0_s\right)$$
14		eqeq1	$$⊢y=A\to \left(y=x{+}_s{1}_s\leftrightarrow A=x{+}_s{1}_s\right)$$
15	14	rexbidv	$$⊢y=A\to \left(\exists x\in {\mathbb{N}}_{\mathrm{0s}}y=x{+}_s{1}_s\leftrightarrow \exists x\in {\mathbb{N}}_{\mathrm{0s}}A=x{+}_s{1}_s\right)$$
16	13 15	orbi12d	$$⊢y=A\to \left(\left(y=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}y=x{+}_s{1}_s\right)\leftrightarrow \left(A=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}A=x{+}_s{1}_s\right)\right)$$
17		eqid	$$⊢0_s=0_s$$
18	17	orci	$$⊢\left(0_s=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}{0}_s=x{+}_s{1}_s\right)$$
19		clel5	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \exists x\in {\mathbb{N}}_{\mathrm{0s}}z=x$$
20	19	biimpi	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \exists x\in {\mathbb{N}}_{\mathrm{0s}}z=x$$
21		n0no	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to z\in \mathrm{No}$$
22		n0no	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in \mathrm{No}$$
23		1no	$$⊢1_s\in \mathrm{No}$$
24		addscan2	$$⊢\left(z\in \mathrm{No}\wedge x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(z{+}_s{1}_s=x{+}_s{1}_s\leftrightarrow z=x\right)$$
25	23 24	mp3an3	$$⊢\left(z\in \mathrm{No}\wedge x\in \mathrm{No}\right)\to \left(z{+}_s{1}_s=x{+}_s{1}_s\leftrightarrow z=x\right)$$
26	21 22 25	syl2an	$$⊢\left(z\in {\mathbb{N}}_{\mathrm{0s}}\wedge x\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z{+}_s{1}_s=x{+}_s{1}_s\leftrightarrow z=x\right)$$
27	26	rexbidva	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\exists x\in {\mathbb{N}}_{\mathrm{0s}}z{+}_s{1}_s=x{+}_s{1}_s\leftrightarrow \exists x\in {\mathbb{N}}_{\mathrm{0s}}z=x\right)$$
28	20 27	mpbird	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \exists x\in {\mathbb{N}}_{\mathrm{0s}}z{+}_s{1}_s=x{+}_s{1}_s$$
29	28	olcd	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \left(z{+}_s{1}_s=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}z{+}_s{1}_s=x{+}_s{1}_s\right)$$
30	29	a1d	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\left(z=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}z=x{+}_s{1}_s\right)\to \left(z{+}_s{1}_s=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}z{+}_s{1}_s=x{+}_s{1}_s\right)\right)$$
31	4 8 12 16 18 30	n0sind	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}A=x{+}_s{1}_s\right)$$