Theorem peano2nns

Description: Peano postulate for positive surreal integers. One plus a positive surreal integer is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	peano2nns	|- ( A e. NN_s -> ( A +s 1s ) e. NN_s )

Proof

Step	Hyp	Ref	Expression
1		1nns	|- 1s e. NN_s
2		nnaddscl	|- ( ( A e. NN_s /\ 1s e. NN_s ) -> ( A +s 1s ) e. NN_s )
3	1 2	mpan2	|- ( A e. NN_s -> ( A +s 1s ) e. NN_s )