Definition df-abss

Description: Define the surreal absolute value function. See abssval for its value and absscl for its closure. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	df-abss	$$⊢{abs}_s=\left(x\in \mathrm{No}⟼if\left(0_s{\le }_{s}x,x,{+}_s\left(x\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabss	$$class{abs}_s$$
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		c0s	$$class{0}_s$$
4		cles	$$class{\le }_s$$
5	1	cv	$$setvarx$$
6	3 5 4	wbr	$$wff{0}_s{\le }_{s}x$$
7		cnegs	$$class{+}_s$$
8	5 7	cfv	$$class{+}_s\left(x\right)$$
9	6 5 8	cif	$$classif\left(0_s{\le }_{s}x,x,{+}_s\left(x\right)\right)$$
10	1 2 9	cmpt	$$class\left(x\in \mathrm{No}⟼if\left(0_s{\le }_{s}x,x,{+}_s\left(x\right)\right)\right)$$
11	0 10	wceq	$$wff{abs}_s=\left(x\in \mathrm{No}⟼if\left(0_s{\le }_{s}x,x,{+}_s\left(x\right)\right)\right)$$