Metamath Proof Explorer

Definition df-nns

Description: Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

Ref Expression
Assertion df-nns 
|- NN_s = ( NN0_s \ { 0s } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnns 
 |-  NN_s
1 cnn0s 
 |-  NN0_s
2 c0s 
 |-  0s
3 2 csn 
 |-  { 0s }
4 1 3 cdif 
 |-  ( NN0_s \ { 0s } )
5 0 4 wceq 
 |-  NN_s = ( NN0_s \ { 0s } )