Theorem sgnfo

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

	Ref	Expression
Assertion	sgnfo	⊢ sgn : ℝ* –onto→ { - 1 , 0 , 1 }

Proof

Step	Hyp	Ref	Expression
1		df-sgn	⊢ sgn = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) )
2	1	funmpt2	⊢ Fun sgn
3		sgndm	⊢ dom sgn = ℝ*
4		df-fn	⊢ ( sgn Fn ℝ* ↔ ( Fun sgn ∧ dom sgn = ℝ* ) )
5	2 3 4	mpbir2an	⊢ sgn Fn ℝ*
6		sgnrn	⊢ ran sgn = { - 1 , 0 , 1 }
7		df-fo	⊢ ( sgn : ℝ* –onto→ { - 1 , 0 , 1 } ↔ ( sgn Fn ℝ* ∧ ran sgn = { - 1 , 0 , 1 } ) )
8	5 6 7	mpbir2an	⊢ sgn : ℝ* –onto→ { - 1 , 0 , 1 }