Theorem subsfn

Description: Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025)

	Ref	Expression
Assertion	subsfn	$$⊢{-}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-subs	$$⊢{-}_s=\left(x\in \mathrm{No},y\in \mathrm{No}⟼x{+}_s{+}_s\left(y\right)\right)$$
2		ovex	$$⊢x{+}_s{+}_s\left(y\right)\in \mathrm{V}$$
3	1 2	fnmpoi	$$⊢{-}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)$$