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 X. No )

Proof

Step Hyp Ref Expression
1 df-subs 
 |-  -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) )
2 ovex 
 |-  ( x +s ( -us ` y ) ) e. _V
3 1 2 fnmpoi 
 |-  -s Fn ( No X. No )