Theorem sgnfo

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

	Ref	Expression
Assertion	sgnfo	|- sgn : RR* -onto-> { -u 1 , 0 , 1 }

Proof

Step	Hyp	Ref	Expression
1		df-sgn	|- sgn = ( x e. RR* |-> if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) )
2	1	funmpt2	|- Fun sgn
3		sgndm	|- dom sgn = RR*
4		df-fn	|- ( sgn Fn RR* <-> ( Fun sgn /\ dom sgn = RR* ) )
5	2 3 4	mpbir2an	|- sgn Fn RR*
6		sgnrn	|- ran sgn = { -u 1 , 0 , 1 }
7		df-fo	|- ( sgn : RR* -onto-> { -u 1 , 0 , 1 } <-> ( sgn Fn RR* /\ ran sgn = { -u 1 , 0 , 1 } ) )
8	5 6 7	mpbir2an	|- sgn : RR* -onto-> { -u 1 , 0 , 1 }