Metamath Proof Explorer

Definition df-zs

Description: Define the surreal integers. Compare dfz2 . (Contributed by Scott Fenton, 17-May-2025)

Ref Expression
Assertion df-zs 
|- ZZ_s = ( -s " ( NN_s X. NN_s ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 czs 
 |-  ZZ_s
1 csubs 
 |-  -s
2 cnns 
 |-  NN_s
3 2 2 cxp 
 |-  ( NN_s X. NN_s )
4 1 3 cima 
 |-  ( -s " ( NN_s X. NN_s ) )
5 0 4 wceq 
 |-  ZZ_s = ( -s " ( NN_s X. NN_s ) )