Theorem negs11

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

	Ref	Expression
Assertion	negs11	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left({+}_s\left(A\right)={+}_s\left(B\right)\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢{+}_s\left(A\right)={+}_s\left(B\right)\to {+}_s\left({+}_s\left(A\right)\right)={+}_s\left({+}_s\left(B\right)\right)$$
2		negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$
3		negnegs	$$⊢B\in \mathrm{No}\to {+}_s\left({+}_s\left(B\right)\right)=B$$
4	2 3	eqeqan12d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left({+}_s\left({+}_s\left(A\right)\right)={+}_s\left({+}_s\left(B\right)\right)\leftrightarrow A=B\right)$$
5	1 4	imbitrid	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left({+}_s\left(A\right)={+}_s\left(B\right)\to A=B\right)$$
6		fveq2	$$⊢A=B\to {+}_s\left(A\right)={+}_s\left(B\right)$$
7	5 6	impbid1	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left({+}_s\left(A\right)={+}_s\left(B\right)\leftrightarrow A=B\right)$$