Metamath Proof Explorer

Theorem rellycmp

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

Ref Expression
Assertion rellycmp ⊢ topGen ⁡ ran ⁡ . ∈ N-Locally Comp

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
2 1 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
3 1 cnllycmp ⊢ TopOpen ⁡ ℂ fld ∈ N-Locally Comp
4 1 recld2 ⊢ ℝ ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
5 cldllycmp ⊢ TopOpen ⁡ ℂ fld ∈ N-Locally Comp ∧ ℝ ∈ Clsd ⁡ TopOpen ⁡ ℂ fld → TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ∈ N-Locally Comp
6 3 4 5 mp2an ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ∈ N-Locally Comp
7 2 6 eqeltri ⊢ topGen ⁡ ran ⁡ . ∈ N-Locally Comp