Theorem negsfo

Description: Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negsfo	$$⊢{+}_s:\mathrm{No}\underset{onto}{⟶}\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		negsf	$$⊢{+}_s:\mathrm{No}⟶\mathrm{No}$$
2		negscl	$$⊢x\in \mathrm{No}\to {+}_s\left(x\right)\in \mathrm{No}$$
3		negnegs	$$⊢x\in \mathrm{No}\to {+}_s\left({+}_s\left(x\right)\right)=x$$
4	3	eqcomd	$$⊢x\in \mathrm{No}\to x={+}_s\left({+}_s\left(x\right)\right)$$
5		fveq2	$$⊢y={+}_s\left(x\right)\to {+}_s\left(y\right)={+}_s\left({+}_s\left(x\right)\right)$$
6	5	eqeq2d	$$⊢y={+}_s\left(x\right)\to \left(x={+}_s\left(y\right)\leftrightarrow x={+}_s\left({+}_s\left(x\right)\right)\right)$$
7	6	rspcev	$$⊢\left({+}_s\left(x\right)\in \mathrm{No}\wedge x={+}_s\left({+}_s\left(x\right)\right)\right)\to \exists y\in \mathrm{No}x={+}_s\left(y\right)$$
8	2 4 7	syl2anc	$$⊢x\in \mathrm{No}\to \exists y\in \mathrm{No}x={+}_s\left(y\right)$$
9	8	rgen	$$⊢\forall x\in \mathrm{No}\exists y\in \mathrm{No}x={+}_s\left(y\right)$$
10		dffo3	$$⊢{+}_s:\mathrm{No}\underset{onto}{⟶}\mathrm{No}\leftrightarrow \left({+}_s:\mathrm{No}⟶\mathrm{No}\wedge \forall x\in \mathrm{No}\exists y\in \mathrm{No}x={+}_s\left(y\right)\right)$$
11	1 9 10	mpbir2an	$$⊢{+}_s:\mathrm{No}\underset{onto}{⟶}\mathrm{No}$$