Theorem subsfo

Description: Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	subsfo	$$⊢{-}_s:\mathrm{No}\times \mathrm{No}\underset{onto}{⟶}\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		subsf	$$⊢{-}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}$$
2		0sno	$$⊢0_s\in \mathrm{No}$$
3		opelxpi	$$⊢\left(x\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to ⟨x,0_s⟩\in \left(\mathrm{No}\times \mathrm{No}\right)$$
4	2 3	mpan2	$$⊢x\in \mathrm{No}\to ⟨x,0_s⟩\in \left(\mathrm{No}\times \mathrm{No}\right)$$
5		subsval	$$⊢\left(x\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to x{-}_s{0}_s=x{+}_s{+}_s\left(0_s\right)$$
6	2 5	mpan2	$$⊢x\in \mathrm{No}\to x{-}_s{0}_s=x{+}_s{+}_s\left(0_s\right)$$
7		negs0s	$$⊢{+}_s\left(0_s\right)=0_s$$
8	7	oveq2i	$$⊢x{+}_s{+}_s\left(0_s\right)=x{+}_s{0}_s$$
9		addsrid	$$⊢x\in \mathrm{No}\to x{+}_s{0}_s=x$$
10	8 9	eqtrid	$$⊢x\in \mathrm{No}\to x{+}_s{+}_s\left(0_s\right)=x$$
11	6 10	eqtr2d	$$⊢x\in \mathrm{No}\to x=x{-}_s{0}_s$$
12		fveq2	$$⊢y=⟨x,0_s⟩\to {-}_s\left(y\right)={-}_s\left(⟨x,0_s⟩\right)$$
13		df-ov	$$⊢x{-}_s{0}_s={-}_s\left(⟨x,0_s⟩\right)$$
14	12 13	eqtr4di	$$⊢y=⟨x,0_s⟩\to {-}_s\left(y\right)=x{-}_s{0}_s$$
15	14	rspceeqv	$$⊢\left(⟨x,0_s⟩\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge x=x{-}_s{0}_s\right)\to \exists y\in \left(\mathrm{No}\times \mathrm{No}\right)x={-}_s\left(y\right)$$
16	4 11 15	syl2anc	$$⊢x\in \mathrm{No}\to \exists y\in \left(\mathrm{No}\times \mathrm{No}\right)x={-}_s\left(y\right)$$
17	16	rgen	$$⊢\forall x\in \mathrm{No}\exists y\in \left(\mathrm{No}\times \mathrm{No}\right)x={-}_s\left(y\right)$$
18		dffo3	$$⊢{-}_s:\mathrm{No}\times \mathrm{No}\underset{onto}{⟶}\mathrm{No}\leftrightarrow \left({-}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}\wedge \forall x\in \mathrm{No}\exists y\in \left(\mathrm{No}\times \mathrm{No}\right)x={-}_s\left(y\right)\right)$$
19	1 17 18	mpbir2an	$$⊢{-}_s:\mathrm{No}\times \mathrm{No}\underset{onto}{⟶}\mathrm{No}$$