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	Could not format assertion : No typesetting found for |- ( A e. No -> ( -us ` A ) e. No ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
2		negsprop	Could not format ( ( A e. No /\ 0s e. No ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` 0s ) ( ( -us ` A ) e. No /\ ( A ( -us ` 0s )
3	1 2	mpan2	Could not format ( A e. No -> ( ( -us ` A ) e. No /\ ( A ( -us ` 0s ) ( ( -us ` A ) e. No /\ ( A ( -us ` 0s )
4	3	simpld	Could not format ( A e. No -> ( -us ` A ) e. No ) : No typesetting found for |- ( A e. No -> ( -us ` A ) e. No ) with typecode |-