Theorem subsf

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

	Ref	Expression
Assertion	subsf	$$⊢{-}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		negscl	$$⊢y\in \mathrm{No}\to {+}_s\left(y\right)\in \mathrm{No}$$
2		addscl	$$⊢\left(x\in \mathrm{No}\wedge {+}_s\left(y\right)\in \mathrm{No}\right)\to x{+}_s{+}_s\left(y\right)\in \mathrm{No}$$
3	1 2	sylan2	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to x{+}_s{+}_s\left(y\right)\in \mathrm{No}$$
4	3	rgen2	$$⊢\forall x\in \mathrm{No}\forall y\in \mathrm{No}x{+}_s{+}_s\left(y\right)\in \mathrm{No}$$
5		df-subs	$$⊢{-}_s=\left(x\in \mathrm{No},y\in \mathrm{No}⟼x{+}_s{+}_s\left(y\right)\right)$$
6	5	fmpo	$$⊢\forall x\in \mathrm{No}\forall y\in \mathrm{No}x{+}_s{+}_s\left(y\right)\in \mathrm{No}\leftrightarrow {-}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}$$
7	4 6	mpbi	$$⊢{-}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}$$