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 ( No × No )

Proof

Step	Hyp	Ref	Expression
1		df-subs	⊢ -s = ( 𝑥 ∈ No , 𝑦 ∈ No ↦ ( 𝑥 +s ( -us ‘ 𝑦 ) ) )
2		ovex	⊢ ( 𝑥 +s ( -us ‘ 𝑦 ) ) ∈ V
3	1 2	fnmpoi	⊢ -s Fn ( No × No )