Metamath Proof Explorer


Theorem negsfn

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

Ref Expression
Assertion negsfn + s Fn No

Proof

Step Hyp Ref Expression
1 df-negs + s = norec s #A# x V , n V n R x | s n L x
2 1 norecfn + s Fn No