Metamath Proof Explorer

Theorem zsex

Description: The surreal integers form a set. (Contributed by Scott Fenton, 17-May-2025)

Ref Expression
Assertion zsex 
|- ZZ_s e. _V

Proof

Step Hyp Ref Expression
1 df-zs 
 |-  ZZ_s = ( -s " ( NN_s X. NN_s ) )
2 subsfn 
 |-  -s Fn ( No X. No )
3 fnfun 
 |-  ( -s Fn ( No X. No ) -> Fun -s )
4 nnsex 
 |-  NN_s e. _V
5 4 4 xpex 
 |-  ( NN_s X. NN_s ) e. _V
6 5 funimaex 
 |-  ( Fun -s -> ( -s " ( NN_s X. NN_s ) ) e. _V )
7 2 3 6 mp2b 
 |-  ( -s " ( NN_s X. NN_s ) ) e. _V
8 1 7 eqeltri 
 |-  ZZ_s e. _V