Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sgns Structured version   Unicode version

Definition df-sgns 27540
Description: Signum function for a structure. See also df-sgn 12900 for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018.)
Assertion
Ref Expression
df-sgns  |- sgns  =  (
r  e.  _V  |->  ( x  e.  ( Base `  r )  |->  if ( x  =  ( 0g
`  r ) ,  0 ,  if ( ( 0g `  r
) ( lt `  r ) x ,  1 ,  -u 1
) ) ) )
Distinct variable group:    x, r

Detailed syntax breakdown of Definition df-sgns
StepHypRef Expression
1 csgns 27539 . 2  class sgns
2 vr . . 3  setvar  r
3 cvv 3118 . . 3  class  _V
4 vx . . . 4  setvar  x
52cv 1378 . . . . 5  class  r
6 cbs 14507 . . . . 5  class  Base
75, 6cfv 5594 . . . 4  class  ( Base `  r )
84cv 1378 . . . . . 6  class  x
9 c0g 14712 . . . . . . 7  class  0g
105, 9cfv 5594 . . . . . 6  class  ( 0g
`  r )
118, 10wceq 1379 . . . . 5  wff  x  =  ( 0g `  r
)
12 cc0 9504 . . . . 5  class  0
13 cplt 15445 . . . . . . . 8  class  lt
145, 13cfv 5594 . . . . . . 7  class  ( lt
`  r )
1510, 8, 14wbr 4453 . . . . . 6  wff  ( 0g
`  r ) ( lt `  r ) x
16 c1 9505 . . . . . 6  class  1
1716cneg 9818 . . . . . 6  class  -u 1
1815, 16, 17cif 3945 . . . . 5  class  if ( ( 0g `  r
) ( lt `  r ) x ,  1 ,  -u 1
)
1911, 12, 18cif 3945 . . . 4  class  if ( x  =  ( 0g
`  r ) ,  0 ,  if ( ( 0g `  r
) ( lt `  r ) x ,  1 ,  -u 1
) )
204, 7, 19cmpt 4511 . . 3  class  ( x  e.  ( Base `  r
)  |->  if ( x  =  ( 0g `  r ) ,  0 ,  if ( ( 0g `  r ) ( lt `  r
) x ,  1 ,  -u 1 ) ) )
212, 3, 20cmpt 4511 . 2  class  ( r  e.  _V  |->  ( x  e.  ( Base `  r
)  |->  if ( x  =  ( 0g `  r ) ,  0 ,  if ( ( 0g `  r ) ( lt `  r
) x ,  1 ,  -u 1 ) ) ) )
221, 21wceq 1379 1  wff sgns  =  (
r  e.  _V  |->  ( x  e.  ( Base `  r )  |->  if ( x  =  ( 0g
`  r ) ,  0 ,  if ( ( 0g `  r
) ( lt `  r ) x ,  1 ,  -u 1
) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  sgnsv  27541
  Copyright terms: Public domain W3C validator