Theorem subsf

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

	Ref	Expression
Assertion	subsf	|- -s : ( No X. No ) --> No

Proof

Step	Hyp	Ref	Expression
1		negscl	|- ( y e. No -> ( -us ` y ) e. No )
2		addscl	|- ( ( x e. No /\ ( -us ` y ) e. No ) -> ( x +s ( -us ` y ) ) e. No )
3	1 2	sylan2	|- ( ( x e. No /\ y e. No ) -> ( x +s ( -us ` y ) ) e. No )
4	3	rgen2	|- A. x e. No A. y e. No ( x +s ( -us ` y ) ) e. No
5		df-subs	|- -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) )
6	5	fmpo	|- ( A. x e. No A. y e. No ( x +s ( -us ` y ) ) e. No <-> -s : ( No X. No ) --> No )
7	4 6	mpbi	|- -s : ( No X. No ) --> No