Theorem sgnsf

Description: The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypotheses	sgnsval.b	$$⊢B={\mathrm{Base}}_R$$
	sgnsval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	sgnsval.l	$$⊢\underset{\dot{}}{<}={<}_R$$
	sgnsval.s	$$⊢S={sgn}_s\left(R\right)$$
Assertion	sgnsf	$$⊢R\in V\to S:B⟶\left\{-1,0,1\right\}$$

Proof

Step	Hyp	Ref	Expression
1		sgnsval.b	$$⊢B={\mathrm{Base}}_R$$
2		sgnsval.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		sgnsval.l	$$⊢\underset{\dot{}}{<}={<}_R$$
4		sgnsval.s	$$⊢S={sgn}_s\left(R\right)$$
5	1 2 3 4	sgnsv	$$⊢R\in V\to S=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)\right)$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7	6	tpid2	$$⊢0\in \left\{-1,0,1\right\}$$
8		1ex	$$⊢1\in \mathrm{V}$$
9	8	tpid3	$$⊢1\in \left\{-1,0,1\right\}$$
10		negex	$$⊢-1\in \mathrm{V}$$
11	10	tpid1	$$⊢-1\in \left\{-1,0,1\right\}$$
12	9 11	ifcli	$$⊢if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\in \left\{-1,0,1\right\}$$
13	7 12	ifcli	$$⊢if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)\in \left\{-1,0,1\right\}$$
14	13	a1i	$$⊢\left(R\in V\wedge x\in B\right)\to if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)\in \left\{-1,0,1\right\}$$
15	5 14	fmpt3d	$$⊢R\in V\to S:B⟶\left\{-1,0,1\right\}$$