Theorem n0p1nns

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

	Ref	Expression
Assertion	n0p1nns	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s\in {\mathbb{N}}_s$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=0_s\to x{+}_s{1}_s=0_s{+}_s{1}_s$$
2	1	eleq1d	$$⊢x=0_s\to \left(x{+}_s{1}_s\in {\mathbb{N}}_s\leftrightarrow 0_s{+}_s{1}_s\in {\mathbb{N}}_s\right)$$
3		oveq1	$$⊢x=y\to x{+}_s{1}_s=y{+}_s{1}_s$$
4	3	eleq1d	$$⊢x=y\to \left(x{+}_s{1}_s\in {\mathbb{N}}_s\leftrightarrow y{+}_s{1}_s\in {\mathbb{N}}_s\right)$$
5		oveq1	$$⊢x=y{+}_s{1}_s\to x{+}_s{1}_s=\left(y{+}_s{1}_s\right){+}_s{1}_s$$
6	5	eleq1d	$$⊢x=y{+}_s{1}_s\to \left(x{+}_s{1}_s\in {\mathbb{N}}_s\leftrightarrow \left(y{+}_s{1}_s\right){+}_s{1}_s\in {\mathbb{N}}_s\right)$$
7		oveq1	$$⊢x=A\to x{+}_s{1}_s=A{+}_s{1}_s$$
8	7	eleq1d	$$⊢x=A\to \left(x{+}_s{1}_s\in {\mathbb{N}}_s\leftrightarrow A{+}_s{1}_s\in {\mathbb{N}}_s\right)$$
9		1no	$$⊢1_s\in \mathrm{No}$$
10		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
11	9 10	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
12		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
13	11 12	eqeltri	$$⊢0_s{+}_s{1}_s\in {\mathbb{N}}_s$$
14		peano2nns	$$⊢y{+}_s{1}_s\in {\mathbb{N}}_s\to \left(y{+}_s{1}_s\right){+}_s{1}_s\in {\mathbb{N}}_s$$
15	14	a1i	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(y{+}_s{1}_s\in {\mathbb{N}}_s\to \left(y{+}_s{1}_s\right){+}_s{1}_s\in {\mathbb{N}}_s\right)$$
16	2 4 6 8 13 15	n0sind	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s\in {\mathbb{N}}_s$$