Theorem elnns

Description: Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	elnns	⊢ ( 𝐴 ∈ ℕs ↔ ( 𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ) )

Proof

Step	Hyp	Ref	Expression
1		df-nns	⊢ ℕs = ( ℕ0s ∖ { 0s } )
2	1	eleq2i	⊢ ( 𝐴 ∈ ℕs ↔ 𝐴 ∈ ( ℕ0s ∖ { 0s } ) )
3		eldifsn	⊢ ( 𝐴 ∈ ( ℕ0s ∖ { 0s } ) ↔ ( 𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ) )
4	2 3	bitri	⊢ ( 𝐴 ∈ ℕs ↔ ( 𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ) )