Theorem sgnfo

Description: The signum function as onto function. (Contributed by AV, 16-Jun-2026)

	Ref	Expression
Assertion	sgnfo	$$⊢\mathrm{sgn}:{ℝ}^{*}\underset{onto}{⟶}\left\{-1,0,1\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-sgn	$$⊢\mathrm{sgn}=\left(x\in {ℝ}^{*}⟼if\left(x=0,0,if\left(x<0,-1,1\right)\right)\right)$$
2	1	funmpt2	$$⊢\mathrm{Fun}\mathrm{sgn}$$
3		sgndm	$$⊢\mathrm{dom}\mathrm{sgn}={ℝ}^{*}$$
4		df-fn	$$⊢\mathrm{sgn}Fn{ℝ}^{*}\leftrightarrow \left(\mathrm{Fun}\mathrm{sgn}\wedge \mathrm{dom}\mathrm{sgn}={ℝ}^{*}\right)$$
5	2 3 4	mpbir2an	$$⊢\mathrm{sgn}Fn{ℝ}^{*}$$
6		sgnrn	$$⊢\mathrm{ran}\mathrm{sgn}=\left\{-1,0,1\right\}$$
7		df-fo	$$⊢\mathrm{sgn}:{ℝ}^{*}\underset{onto}{⟶}\left\{-1,0,1\right\}\leftrightarrow \left(\mathrm{sgn}Fn{ℝ}^{*}\wedge \mathrm{ran}\mathrm{sgn}=\left\{-1,0,1\right\}\right)$$
8	5 6 7	mpbir2an	$$⊢\mathrm{sgn}:{ℝ}^{*}\underset{onto}{⟶}\left\{-1,0,1\right\}$$