Metamath Proof Explorer

Theorem znegscl

Description: The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025)

Ref Expression
Assertion znegscl 
|- ( A e. ZZ_s -> ( -us ` A ) e. ZZ_s )

Proof

Step Hyp Ref Expression
1 nnsno 
 |-  ( n e. NN_s -> n e. No )
2 1 adantr 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> n e. No )
3 nnsno 
 |-  ( m e. NN_s -> m e. No )
4 3 adantl 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> m e. No )
5 2 4 negsubsdi2d 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( -us ` ( n -s m ) ) = ( m -s n ) )
6 fveqeq2 
 |-  ( A = ( n -s m ) -> ( ( -us ` A ) = ( m -s n ) <-> ( -us ` ( n -s m ) ) = ( m -s n ) ) )
7 5 6 syl5ibrcom 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( A = ( n -s m ) -> ( -us ` A ) = ( m -s n ) ) )
8 7 reximdva 
 |-  ( n e. NN_s -> ( E. m e. NN_s A = ( n -s m ) -> E. m e. NN_s ( -us ` A ) = ( m -s n ) ) )
9 8 reximia 
 |-  ( E. n e. NN_s E. m e. NN_s A = ( n -s m ) -> E. n e. NN_s E. m e. NN_s ( -us ` A ) = ( m -s n ) )
10 elzs 
 |-  ( A e. ZZ_s <-> E. n e. NN_s E. m e. NN_s A = ( n -s m ) )
11 elzs 
 |-  ( ( -us ` A ) e. ZZ_s <-> E. m e. NN_s E. n e. NN_s ( -us ` A ) = ( m -s n ) )
12 rexcom 
 |-  ( E. m e. NN_s E. n e. NN_s ( -us ` A ) = ( m -s n ) <-> E. n e. NN_s E. m e. NN_s ( -us ` A ) = ( m -s n ) )
13 11 12 bitri 
 |-  ( ( -us ` A ) e. ZZ_s <-> E. n e. NN_s E. m e. NN_s ( -us ` A ) = ( m -s n ) )
14 9 10 13 3imtr4i 
 |-  ( A e. ZZ_s -> ( -us ` A ) e. ZZ_s )