Metamath Proof Explorer

Theorem 1zs

Description: One is a surreal integer. (Contributed by Scott Fenton, 24-Jul-2025)

Ref Expression
Assertion 1zs 
|- 1s e. ZZ_s

Proof

Step Hyp Ref Expression
1 1n0s 
 |-  1s e. NN0_s
2 n0zs 
 |-  ( 1s e. NN0_s -> 1s e. ZZ_s )
3 1 2 ax-mp 
 |-  1s e. ZZ_s