Theorem abssor

Description: The absolute value of a surreal is either that surreal or its negative. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	abssor	$$⊢A\in \mathrm{No}\to \left({abs}_s\left(A\right)=A\vee {abs}_s\left(A\right)={+}_s\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ifeqor	$$⊢\left(if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)=A\vee if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)={+}_s\left(A\right)\right)$$
2		abssval	$$⊢A\in \mathrm{No}\to {abs}_s\left(A\right)=if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)$$
3	2	eqeq1d	$$⊢A\in \mathrm{No}\to \left({abs}_s\left(A\right)=A\leftrightarrow if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)=A\right)$$
4	2	eqeq1d	$$⊢A\in \mathrm{No}\to \left({abs}_s\left(A\right)={+}_s\left(A\right)\leftrightarrow if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)={+}_s\left(A\right)\right)$$
5	3 4	orbi12d	$$⊢A\in \mathrm{No}\to \left(\left({abs}_s\left(A\right)=A\vee {abs}_s\left(A\right)={+}_s\left(A\right)\right)\leftrightarrow \left(if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)=A\vee if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)={+}_s\left(A\right)\right)\right)$$
6	1 5	mpbiri	$$⊢A\in \mathrm{No}\to \left({abs}_s\left(A\right)=A\vee {abs}_s\left(A\right)={+}_s\left(A\right)\right)$$