Theorem 2nns

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

	Ref	Expression
Assertion	2nns	Could not format assertion : No typesetting found for |- 2s e. NN_s with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1p1e2s	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-
2		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
3		peano2nns	$$⊢1_s\in {\mathbb{N}}_s\to 1_s{+}_s{1}_s\in {\mathbb{N}}_s$$
4	2 3	ax-mp	$$⊢1_s{+}_s{1}_s\in {\mathbb{N}}_s$$
5	1 4	eqeltrri	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-