Theorem sgnrn

Description: The range of the signum function. (Contributed by AV, 16-Jun-2026) (Proof shortened by TA, 21-Jun-2026)

	Ref	Expression
Assertion	sgnrn	⊢ ran sgn = { - 1 , 0 , 1 }

Proof

Step	Hyp	Ref	Expression
1		df-sgn	⊢ sgn = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) )
2	1	fnmpt	⊢ ( ∀ 𝑥 ∈ ℝ* if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) ∈ { - 1 , 0 , 1 } → sgn Fn ℝ* )
3		sgnval	⊢ ( 𝑥 ∈ ℝ* → ( sgn ‘ 𝑥 ) = if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) )
4		sgncl	⊢ ( 𝑥 ∈ ℝ* → ( sgn ‘ 𝑥 ) ∈ { - 1 , 0 , 1 } )
5	3 4	eqeltrrd	⊢ ( 𝑥 ∈ ℝ* → if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) ∈ { - 1 , 0 , 1 } )
6	2 5	mprg	⊢ sgn Fn ℝ*
7	4	rgen	⊢ ∀ 𝑥 ∈ ℝ* ( sgn ‘ 𝑥 ) ∈ { - 1 , 0 , 1 }
8		fnfvrnss	⊢ ( ( sgn Fn ℝ* ∧ ∀ 𝑥 ∈ ℝ* ( sgn ‘ 𝑥 ) ∈ { - 1 , 0 , 1 } ) → ran sgn ⊆ { - 1 , 0 , 1 } )
9	6 7 8	mp2an	⊢ ran sgn ⊆ { - 1 , 0 , 1 }
10		sgnmnf	⊢ ( sgn ‘ -∞ ) = - 1
11		mnfxr	⊢ -∞ ∈ ℝ*
12		fnfvelrn	⊢ ( ( sgn Fn ℝ* ∧ -∞ ∈ ℝ* ) → ( sgn ‘ -∞ ) ∈ ran sgn )
13	6 11 12	mp2an	⊢ ( sgn ‘ -∞ ) ∈ ran sgn
14	10 13	eqeltrri	⊢ - 1 ∈ ran sgn
15		sgn0	⊢ ( sgn ‘ 0 ) = 0
16		0xr	⊢ 0 ∈ ℝ*
17		fnfvelrn	⊢ ( ( sgn Fn ℝ* ∧ 0 ∈ ℝ* ) → ( sgn ‘ 0 ) ∈ ran sgn )
18	6 16 17	mp2an	⊢ ( sgn ‘ 0 ) ∈ ran sgn
19	15 18	eqeltrri	⊢ 0 ∈ ran sgn
20		sgn1	⊢ ( sgn ‘ 1 ) = 1
21		1xr	⊢ 1 ∈ ℝ*
22		fnfvelrn	⊢ ( ( sgn Fn ℝ* ∧ 1 ∈ ℝ* ) → ( sgn ‘ 1 ) ∈ ran sgn )
23	6 21 22	mp2an	⊢ ( sgn ‘ 1 ) ∈ ran sgn
24	20 23	eqeltrri	⊢ 1 ∈ ran sgn
25		tpssi	⊢ ( ( - 1 ∈ ran sgn ∧ 0 ∈ ran sgn ∧ 1 ∈ ran sgn ) → { - 1 , 0 , 1 } ⊆ ran sgn )
26	14 19 24 25	mp3an	⊢ { - 1 , 0 , 1 } ⊆ ran sgn
27	9 26	eqssi	⊢ ran sgn = { - 1 , 0 , 1 }