Metamath Proof Explorer


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 = x No , y No x + s + s y
2 ovex x + s + s y V
3 1 2 fnmpoi - s Fn No × No