Metamath Proof Explorer

Definition df-sgns

Description: Signum function for a structure. See also df-sgn for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018)

Ref Expression
Assertion df-sgns ⊢ sgn s = r ∈ V ⟼ x ∈ Base r ⟼ if x = 0 r 0 if 0 r < r x 1 − 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 csgns class sgn s
1 vr setvar r
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar r
6 5 4 cfv class Base r
7 3 cv setvar x
8 c0g class 0 𝑔
9 5 8 cfv class 0 r
10 7 9 wceq wff x = 0 r
11 cc0 class 0
12 cplt class lt
13 5 12 cfv class < r
14 9 7 13 wbr wff 0 r < r x
15 c1 class 1
16 15 cneg class -1
17 14 15 16 cif class if 0 r < r x 1 − 1
18 10 11 17 cif class if x = 0 r 0 if 0 r < r x 1 − 1
19 3 6 18 cmpt class x ∈ Base r ⟼ if x = 0 r 0 if 0 r < r x 1 − 1
20 1 2 19 cmpt class r ∈ V ⟼ x ∈ Base r ⟼ if x = 0 r 0 if 0 r < r x 1 − 1
21 0 20 wceq wff sgn s = r ∈ V ⟼ x ∈ Base r ⟼ if x = 0 r 0 if 0 r < r x 1 − 1