Theorem 2nns

Description: Surreal two is a surreal natural. (Contributed by Scott Fenton, 23-Jul-2025)

	Ref	Expression
Assertion	2nns	⊢ 2s ∈ ℕs

Proof

Step	Hyp	Ref	Expression
1		1p1e2s	⊢ ( 1s +s 1s ) = 2s
2		1nns	⊢ 1s ∈ ℕs
3		peano2nns	⊢ ( 1s ∈ ℕs → ( 1s +s 1s ) ∈ ℕs )
4	2 3	ax-mp	⊢ ( 1s +s 1s ) ∈ ℕs
5	1 4	eqeltrri	⊢ 2s ∈ ℕs