Metamath Proof Explorer


Theorem subsf

Description: Function statement for surreal subtraction. (Contributed by Scott Fenton, 17-May-2025)

Ref Expression
Assertion subsf - s : No × No No

Proof

Step Hyp Ref Expression
1 negscl y No + s y No
2 addscl x No + s y No x + s + s y No
3 1 2 sylan2 x No y No x + s + s y No
4 3 rgen2 x No y No x + s + s y No
5 df-subs - s = x No , y No x + s + s y
6 5 fmpo x No y No x + s + s y No - s : No × No No
7 4 6 mpbi - s : No × No No