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		1sne0s	⊢ 1s ≠ 0s
3		eldifsn	⊢ ( 1s ∈ ( ℕ0s ∖ { 0s } ) ↔ ( 1s ∈ ℕ0s ∧ 1s ≠ 0s ) )
4	1 2 3	mpbir2an	⊢ 1s ∈ ( ℕ0s ∖ { 0s } )
5		df-nns	⊢ ℕs = ( ℕ0s ∖ { 0s } )
6	4 5	eleqtrri	⊢ 1s ∈ ℕs