Theorem n0cut2

Description: A cut form for the successor of a non-negative surreal integer. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	n0cut2	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s=\left\{A\right\}{|}_s\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		peano2n0s	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
2		n0cut	$$⊢A{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s=\left\{\left(A{+}_s{1}_s\right){-}_s{1}_s\right\}{|}_s\varnothing$$
3	1 2	syl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s=\left\{\left(A{+}_s{1}_s\right){-}_s{1}_s\right\}{|}_s\varnothing$$
4		n0no	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in \mathrm{No}$$
5		1no	$$⊢1_s\in \mathrm{No}$$
6		pncans	$$⊢\left(A\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(A{+}_s{1}_s\right){-}_s{1}_s=A$$
7	4 5 6	sylancl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{+}_s{1}_s\right){-}_s{1}_s=A$$
8	7	sneqd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{\left(A{+}_s{1}_s\right){-}_s{1}_s\right\}=\left\{A\right\}$$
9	8	oveq1d	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{\left(A{+}_s{1}_s\right){-}_s{1}_s\right\}{|}_s\varnothing =\left\{A\right\}{|}_s\varnothing$$
10	3 9	eqtrd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s=\left\{A\right\}{|}_s\varnothing$$