Theorem rellycmp

Description: The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	rellycmp	⊢ ( topGen ‘ ran (,) ) ∈ 𝑛-Locally Comp

Proof

Step	Hyp	Ref	Expression
1		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
2		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3	2	cnllycmp	⊢ ( TopOpen ‘ ℂfld ) ∈ 𝑛-Locally Comp
4	2	recld2	⊢ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) )
5		cldllycmp	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ 𝑛-Locally Comp ∧ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ∈ 𝑛-Locally Comp )
6	3 4 5	mp2an	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ∈ 𝑛-Locally Comp
7	1 6	eqeltri	⊢ ( topGen ‘ ran (,) ) ∈ 𝑛-Locally Comp