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	⊢ ( 𝐴 ∈ ℕs → ( 𝐴 +s 1s ) ∈ ℕs )

Proof

Step	Hyp	Ref	Expression
1		1nns	⊢ 1s ∈ ℕs
2		nnaddscl	⊢ ( ( 𝐴 ∈ ℕs ∧ 1s ∈ ℕs ) → ( 𝐴 +s 1s ) ∈ ℕs )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℕs → ( 𝐴 +s 1s ) ∈ ℕs )