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 " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) )
2	1	norecfn	|- -us Fn No