Metamath Proof Explorer

Theorem 1nns

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

Ref Expression
Assertion 1nns 
|- 1s e. NN_s

Proof

Step Hyp Ref Expression
1 1n0s 
 |-  1s e. NN0_s
2 1sne0s 
 |-  1s =/= 0s
3 eldifsn 
 |-  ( 1s e. ( NN0_s \ { 0s } ) <-> ( 1s e. NN0_s /\ 1s =/= 0s ) )
4 1 2 3 mpbir2an 
 |-  1s e. ( NN0_s \ { 0s } )
5 df-nns 
 |-  NN_s = ( NN0_s \ { 0s } )
6 4 5 eleqtrri 
 |-  1s e. NN_s