Metamath Proof Explorer

Theorem elzs

Description: Membership in the set of surreal integers. (Contributed by Scott Fenton, 17-May-2025)

Ref Expression
Assertion elzs 
|- ( A e. ZZ_s <-> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )

Proof

Step Hyp Ref Expression
1 df-zs 
 |-  ZZ_s = ( -s " ( NN_s X. NN_s ) )
2 1 eleq2i 
 |-  ( A e. ZZ_s <-> A e. ( -s " ( NN_s X. NN_s ) ) )
3 subsfn 
 |-  -s Fn ( No X. No )
4 nnssno 
 |-  NN_s C_ No
5 xpss12 
 |-  ( ( NN_s C_ No /\ NN_s C_ No ) -> ( NN_s X. NN_s ) C_ ( No X. No ) )
6 4 4 5 mp2an 
 |-  ( NN_s X. NN_s ) C_ ( No X. No )
7 ovelimab 
 |-  ( ( -s Fn ( No X. No ) /\ ( NN_s X. NN_s ) C_ ( No X. No ) ) -> ( A e. ( -s " ( NN_s X. NN_s ) ) <-> E. x e. NN_s E. y e. NN_s A = ( x -s y ) ) )
8 3 6 7 mp2an 
 |-  ( A e. ( -s " ( NN_s X. NN_s ) ) <-> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )
9 2 8 bitri 
 |-  ( A e. ZZ_s <-> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )