Metamath Proof Explorer

Theorem nnsex

Description: The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025)

Ref Expression
Assertion nnsex 
|- NN_s e. _V

Proof

Step Hyp Ref Expression
1 df-nns 
 |-  NN_s = ( NN0_s \ { 0s } )
2 n0sex 
 |-  NN0_s e. _V
3 2 difexi 
 |-  ( NN0_s \ { 0s } ) e. _V
4 1 3 eqeltri 
 |-  NN_s e. _V