Metamath Proof Explorer

Theorem negscl

Description: The surreals are closed under negation. Theorem 6(ii) of Conway p. 18. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negscl 
|- ( A e. No -> ( -us ` A ) e. No )

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 negsprop 
 |-  ( ( A e. No /\ 0s e. No ) -> ( ( -us ` A ) e. No /\ ( A  ( -us ` 0s )
3 1 2 mpan2 
 |-  ( A e. No -> ( ( -us ` A ) e. No /\ ( A  ( -us ` 0s )
4 3 simpld 
 |-  ( A e. No -> ( -us ` A ) e. No )