Theorem negsf1o

Description: Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negsf1o	$$⊢{+}_s:\mathrm{No}\underset{1-1\; onto}{⟶}\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		negsf	$$⊢{+}_s:\mathrm{No}⟶\mathrm{No}$$
2		negs11	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to \left({+}_s\left(x\right)={+}_s\left(y\right)\leftrightarrow x=y\right)$$
3	2	biimpd	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to \left({+}_s\left(x\right)={+}_s\left(y\right)\to x=y\right)$$
4	3	rgen2	$$⊢\forall x\in \mathrm{No}\forall y\in \mathrm{No}\left({+}_s\left(x\right)={+}_s\left(y\right)\to x=y\right)$$
5		dff13	$$⊢{+}_s:\mathrm{No}\underset{1-1}{⟶}\mathrm{No}\leftrightarrow \left({+}_s:\mathrm{No}⟶\mathrm{No}\wedge \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left({+}_s\left(x\right)={+}_s\left(y\right)\to x=y\right)\right)$$
6	1 4 5	mpbir2an	$$⊢{+}_s:\mathrm{No}\underset{1-1}{⟶}\mathrm{No}$$
7		negsfo	$$⊢{+}_s:\mathrm{No}\underset{onto}{⟶}\mathrm{No}$$
8		df-f1o	$$⊢{+}_s:\mathrm{No}\underset{1-1\; onto}{⟶}\mathrm{No}\leftrightarrow \left({+}_s:\mathrm{No}\underset{1-1}{⟶}\mathrm{No}\wedge {+}_s:\mathrm{No}\underset{onto}{⟶}\mathrm{No}\right)$$
9	6 7 8	mpbir2an	$$⊢{+}_s:\mathrm{No}\underset{1-1\; onto}{⟶}\mathrm{No}$$