Theorem 1nns

Description: Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	1nns	⊢ 1s ∈ ℕs

Proof

Step	Hyp	Ref	Expression
1		1n0s	⊢ 1s ∈ ℕ0s
2		0slt1s	⊢ 0s <s 1s
3		sgt0ne0	⊢ ( 0s <s 1s → 1s ≠ 0s )
4	2 3	ax-mp	⊢ 1s ≠ 0s
5		eldifsn	⊢ ( 1s ∈ ( ℕ0s ∖ { 0s } ) ↔ ( 1s ∈ ℕ0s ∧ 1s ≠ 0s ) )
6	1 4 5	mpbir2an	⊢ 1s ∈ ( ℕ0s ∖ { 0s } )
7		df-nns	⊢ ℕs = ( ℕ0s ∖ { 0s } )
8	6 7	eleqtrri	⊢ 1s ∈ ℕs