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	⊢ abss = ( 𝑥 ∈ No ↦ if ( 0s ≤s 𝑥 , 𝑥 , ( -us ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabss	⊢ abss
1		vx	⊢ 𝑥
2		csur	⊢ No
3		c0s	⊢ 0s
4		csle	⊢ ≤s
5	1	cv	⊢ 𝑥
6	3 5 4	wbr	⊢ 0s ≤s 𝑥
7		cnegs	⊢ -us
8	5 7	cfv	⊢ ( -us ‘ 𝑥 )
9	6 5 8	cif	⊢ if ( 0s ≤s 𝑥 , 𝑥 , ( -us ‘ 𝑥 ) )
10	1 2 9	cmpt	⊢ ( 𝑥 ∈ No ↦ if ( 0s ≤s 𝑥 , 𝑥 , ( -us ‘ 𝑥 ) ) )
11	0 10	wceq	⊢ abss = ( 𝑥 ∈ No ↦ if ( 0s ≤s 𝑥 , 𝑥 , ( -us ‘ 𝑥 ) ) )