Theorem n0scut2

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

	Ref	Expression
Assertion	n0scut2	|- ( A e. NN0_s -> ( A +s 1s ) = ( { A } |s (/) ) )

Proof

Step	Hyp	Ref	Expression
1		peano2n0s	|- ( A e. NN0_s -> ( A +s 1s ) e. NN0_s )
2		n0scut	|- ( ( A +s 1s ) e. NN0_s -> ( A +s 1s ) = ( { ( ( A +s 1s ) -s 1s ) } |s (/) ) )
3	1 2	syl	|- ( A e. NN0_s -> ( A +s 1s ) = ( { ( ( A +s 1s ) -s 1s ) } |s (/) ) )
4		n0sno	|- ( A e. NN0_s -> A e. No )
5		1sno	|- 1s e. No
6		pncans	|- ( ( A e. No /\ 1s e. No ) -> ( ( A +s 1s ) -s 1s ) = A )
7	4 5 6	sylancl	|- ( A e. NN0_s -> ( ( A +s 1s ) -s 1s ) = A )
8	7	sneqd	|- ( A e. NN0_s -> { ( ( A +s 1s ) -s 1s ) } = { A } )
9	8	oveq1d	|- ( A e. NN0_s -> ( { ( ( A +s 1s ) -s 1s ) } |s (/) ) = ( { A } |s (/) ) )
10	3 9	eqtrd	|- ( A e. NN0_s -> ( A +s 1s ) = ( { A } |s (/) ) )