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 0slt1s 
 |-  0s
3 sgt0ne0 
 |-  ( 0s  1s =/= 0s )
4 2 3 ax-mp 
 |-  1s =/= 0s
5 eldifsn 
 |-  ( 1s e. ( NN0_s \ { 0s } ) <-> ( 1s e. NN0_s /\ 1s =/= 0s ) )
6 1 4 5 mpbir2an 
 |-  1s e. ( NN0_s \ { 0s } )
7 df-nns 
 |-  NN_s = ( NN0_s \ { 0s } )
8 6 7 eleqtrri 
 |-  1s e. NN_s