Theorem rehaus

Description: The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007)

	Ref	Expression
Assertion	rehaus	⊢ ( topGen ‘ ran (,) ) ∈ Haus

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2	1	rexmet	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
3		eqid	⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
4	1 3	tgioo	⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
5	4	methaus	⊢ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) → ( topGen ‘ ran (,) ) ∈ Haus )
6	2 5	ax-mp	⊢ ( topGen ‘ ran (,) ) ∈ Haus