Definition df-abss 28280

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

Assertion

Ref	Expression
df-abss	⊢ abss = (𝑥 ∈ No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥)))

Detailed syntax breakdown of Definition df-abss

Step	Hyp	Ref	Expression
1		cabss 28279	. 2 class abss
2		vx	. . 3 setvar 𝑥
3		csur 27702	. . 3 class No
4		c0s 27885	. . . . 5 class 0s
5	2	cv 1536	. . . . 5 class 𝑥
6		csle 27807	. . . . 5 class ≤s
7	4, 5, 6	wbr 5166	. . . 4 wff 0s ≤s 𝑥
8		cnegs 28069	. . . . 5 class -us
9	5, 8	cfv 6573	. . . 4 class ( -us ‘𝑥)
10	7, 5, 9	cif 4548	. . 3 class if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥))
11	2, 3, 10	cmpt 5249	. 2 class (𝑥 ∈ No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥)))
12	1, 11	wceq 1537	1 wff abss = (𝑥 ∈ No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥)))

This definition is referenced by:  abssval  28281