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 tgioo4 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 2 cnllycmp ⊢ TopOpen ⁡ ℂ fld ∈ N-Locally Comp
4 2 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 1 6 eqeltri ⊢ topGen ⁡ ran ⁡ . ∈ N-Locally Comp