Theorem negsfn

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

	Ref	Expression
Assertion	negsfn	Could not format assertion : No typesetting found for |- -us Fn No with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-negs	Could not format -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ) : No typesetting found for |- -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ) with typecode |-
2	1	norecfn	Could not format -us Fn No : No typesetting found for |- -us Fn No with typecode |-