Metamath Proof Explorer

Theorem n0zs

Description: A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025)

Ref Expression
Assertion n0zs 
|- ( A e. NN0_s -> A e. ZZ_s )

Proof

Step Hyp Ref Expression
1 eln0s 
 |-  ( A e. NN0_s <-> ( A e. NN_s \/ A = 0s ) )
2 nnzs 
 |-  ( A e. NN_s -> A e. ZZ_s )
3 id 
 |-  ( A = 0s -> A = 0s )
4 0zs 
 |-  0s e. ZZ_s
5 3 4 eqeltrdi 
 |-  ( A = 0s -> A e. ZZ_s )
6 2 5 jaoi 
 |-  ( ( A e. NN_s \/ A = 0s ) -> A e. ZZ_s )
7 1 6 sylbi 
 |-  ( A e. NN0_s -> A e. ZZ_s )