Theorem negsex

Description: Every surreal has a negative. Note that this theorem, addscl , addscom , addsass , addsrid , and ltadds1im are the ordered Abelian group axioms. However, the surreals cannot be said to be an ordered Abelian group because No is a proper class. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negsex	$$⊢A\in \mathrm{No}\to \exists x\in \mathrm{No}A{+}_{s}x=0_s$$

Proof

Step	Hyp	Ref	Expression
1		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
2		negsid	$$⊢A\in \mathrm{No}\to A{+}_s{+}_s\left(A\right)=0_s$$
3		oveq2	$$⊢x={+}_s\left(A\right)\to A{+}_{s}x=A{+}_s{+}_s\left(A\right)$$
4	3	eqeq1d	$$⊢x={+}_s\left(A\right)\to \left(A{+}_{s}x=0_s\leftrightarrow A{+}_s{+}_s\left(A\right)=0_s\right)$$
5	4	rspcev	$$⊢\left({+}_s\left(A\right)\in \mathrm{No}\wedge A{+}_s{+}_s\left(A\right)=0_s\right)\to \exists x\in \mathrm{No}A{+}_{s}x=0_s$$
6	1 2 5	syl2anc	$$⊢A\in \mathrm{No}\to \exists x\in \mathrm{No}A{+}_{s}x=0_s$$