Metamath Proof Explorer

Theorem negsf

Description: Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negsf 
|- -us : No --> No

Proof

Step Hyp Ref Expression
1 negsfn 
 |-  -us Fn No
2 negscl 
 |-  ( x e. No -> ( -us ` x ) e. No )
3 2 rgen 
 |-  A. x e. No ( -us ` x ) e. No
4 ffnfv 
 |-  ( -us : No --> No <-> ( -us Fn No /\ A. x e. No ( -us ` x ) e. No ) )
5 1 3 4 mpbir2an 
 |-  -us : No --> No