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 = ( x e. No |-> if ( 0s <_s x , x , ( -us ` x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabss	|- abs_s
1		vx	|- x
2		csur	|- No
3		c0s	|- 0s
4		csle	|- <_s
5	1	cv	|- x
6	3 5 4	wbr	|- 0s <_s x
7		cnegs	|- -us
8	5 7	cfv	|- ( -us ` x )
9	6 5 8	cif	|- if ( 0s <_s x , x , ( -us ` x ) )
10	1 2 9	cmpt	|- ( x e. No |-> if ( 0s <_s x , x , ( -us ` x ) ) )
11	0 10	wceq	|- abs_s = ( x e. No |-> if ( 0s <_s x , x , ( -us ` x ) ) )