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	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 1s ) = ( { 𝐴 } |s ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		peano2n0s	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 1s ) ∈ ℕ0s )
2		n0scut	⊢ ( ( 𝐴 +s 1s ) ∈ ℕ0s → ( 𝐴 +s 1s ) = ( { ( ( 𝐴 +s 1s ) -s 1s ) } |s ∅ ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 1s ) = ( { ( ( 𝐴 +s 1s ) -s 1s ) } |s ∅ ) )
4		n0sno	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ No )
5		1sno	⊢ 1s ∈ No
6		pncans	⊢ ( ( 𝐴 ∈ No ∧ 1s ∈ No ) → ( ( 𝐴 +s 1s ) -s 1s ) = 𝐴 )
7	4 5 6	sylancl	⊢ ( 𝐴 ∈ ℕ0s → ( ( 𝐴 +s 1s ) -s 1s ) = 𝐴 )
8	7	sneqd	⊢ ( 𝐴 ∈ ℕ0s → { ( ( 𝐴 +s 1s ) -s 1s ) } = { 𝐴 } )
9	8	oveq1d	⊢ ( 𝐴 ∈ ℕ0s → ( { ( ( 𝐴 +s 1s ) -s 1s ) } |s ∅ ) = ( { 𝐴 } |s ∅ ) )
10	3 9	eqtrd	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 1s ) = ( { 𝐴 } |s ∅ ) )