Theorem subsfn

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

	Ref	Expression
Assertion	subsfn	Could not format assertion : No typesetting found for |- -s Fn ( No X. No ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-subs	Could not format -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) ) : No typesetting found for |- -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) ) with typecode |-
2		ovex	Could not format ( x +s ( -us ` y ) ) e. _V : No typesetting found for |- ( x +s ( -us ` y ) ) e. _V with typecode |-
3	1 2	fnmpoi	Could not format -s Fn ( No X. No ) : No typesetting found for |- -s Fn ( No X. No ) with typecode |-