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=\left(r\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_r⟼if\left(x=0_r,0,if\left(0_r{<}_{r}x,1,-1\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgns	$$class{sgn}_s$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Base}}_r$$
7	3	cv	$$setvarx$$
8		c0g	$$class{0}_{𝑔}$$
9	5 8	cfv	$$class{0}_r$$
10	7 9	wceq	$$wffx=0_r$$
11		cc0	$$class0$$
12		cplt	$$class\mathrm{lt}$$
13	5 12	cfv	$$class{<}_r$$
14	9 7 13	wbr	$$wff{0}_r{<}_{r}x$$
15		c1	$$class1$$
16	15	cneg	$$class-1$$
17	14 15 16	cif	$$classif\left(0_r{<}_{r}x,1,-1\right)$$
18	10 11 17	cif	$$classif\left(x=0_r,0,if\left(0_r{<}_{r}x,1,-1\right)\right)$$
19	3 6 18	cmpt	$$class\left(x\in {\mathrm{Base}}_r⟼if\left(x=0_r,0,if\left(0_r{<}_{r}x,1,-1\right)\right)\right)$$
20	1 2 19	cmpt	$$class\left(r\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_r⟼if\left(x=0_r,0,if\left(0_r{<}_{r}x,1,-1\right)\right)\right)\right)$$
21	0 20	wceq	$$wff{sgn}_s=\left(r\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_r⟼if\left(x=0_r,0,if\left(0_r{<}_{r}x,1,-1\right)\right)\right)\right)$$