MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-abss Structured version   Visualization version   GIF version

Definition df-abss 28277
Description: Define the surreal absolute value function. See abssval 28278 for its value and absscl 28279 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
StepHypRef Expression
1 cabss 28276 . 2 class abss
2 vx . . 3 setvar 𝑥
3 csur 27699 . . 3 class No
4 c0s 27882 . . . . 5 class 0s
52cv 1536 . . . . 5 class 𝑥
6 csle 27804 . . . . 5 class ≤s
74, 5, 6wbr 5148 . . . 4 wff 0s ≤s 𝑥
8 cnegs 28066 . . . . 5 class -us
95, 8cfv 6563 . . . 4 class ( -us𝑥)
107, 5, 9cif 4531 . . 3 class if( 0s ≤s 𝑥, 𝑥, ( -us𝑥))
112, 3, 10cmpt 5231 . 2 class (𝑥 No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us𝑥)))
121, 11wceq 1537 1 wff abss = (𝑥 No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  abssval  28278
  Copyright terms: Public domain W3C validator