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 ( ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) )
2	1	norecfn	⊢ -us Fn No