Metamath Proof Explorer

Theorem elnns2

Description: A positive surreal integer is a non-negative surreal integer greater than zero. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion elnns2 
|- ( A e. NN_s <-> ( A e. NN0_s /\ 0s

Proof

Step Hyp Ref Expression
1 elnns 
 |-  ( A e. NN_s <-> ( A e. NN0_s /\ A =/= 0s ) )
2 nesym 
 |-  ( A =/= 0s <-> -. 0s = A )
3 n0sge0 
 |-  ( A e. NN0_s -> 0s <_s A )
4 0sno 
 |-  0s e. No
5 n0sno 
 |-  ( A e. NN0_s -> A e. No )
6 sleloe 
 |-  ( ( 0s e. No /\ A e. No ) -> ( 0s <_s A <-> ( 0s
7 4 5 6 sylancr 
 |-  ( A e. NN0_s -> ( 0s <_s A <-> ( 0s
8 3 7 mpbid 
 |-  ( A e. NN0_s -> ( 0s
9 8 orcomd 
 |-  ( A e. NN0_s -> ( 0s = A \/ 0s
10 9 ord 
 |-  ( A e. NN0_s -> ( -. 0s = A -> 0s
11 2 10 biimtrid 
 |-  ( A e. NN0_s -> ( A =/= 0s -> 0s
12 sgt0ne0 
 |-  ( 0s  A =/= 0s )
13 11 12 impbid1 
 |-  ( A e. NN0_s -> ( A =/= 0s <-> 0s
14 13 pm5.32i 
 |-  ( ( A e. NN0_s /\ A =/= 0s ) <-> ( A e. NN0_s /\ 0s
15 1 14 bitri 
 |-  ( A e. NN_s <-> ( A e. NN0_s /\ 0s