Metamath Proof Explorer

Theorem negsfn

Description: Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion negsfn 
|- -us Fn No

Proof

Step Hyp Ref Expression
1 df-negs 
 |-  -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) )
2 1 norecfn 
 |-  -us Fn No