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\in {\mathbb{N}}_s\to A{+}_s{1}_s\in {\mathbb{N}}_s$$

Proof

Step	Hyp	Ref	Expression
1		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
2		nnaddscl	$$⊢\left(A\in {\mathbb{N}}_s\wedge 1_s\in {\mathbb{N}}_s\right)\to A{+}_s{1}_s\in {\mathbb{N}}_s$$
3	1 2	mpan2	$$⊢A\in {\mathbb{N}}_s\to A{+}_s{1}_s\in {\mathbb{N}}_s$$