Metamath Proof Explorer

Theorem llycmpkgen

Description: A locally compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion llycmpkgen ⊢ J ∈ N-Locally Comp → J ∈ ran ⁡ 𝑘Gen

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 nllytop ⊢ J ∈ N-Locally Comp → J ∈ Top
3 simpl ⊢ J ∈ N-Locally Comp ∧ x ∈ ⋃ J → J ∈ N-Locally Comp
4 1 topopn ⊢ J ∈ Top → ⋃ J ∈ J
5 2 4 syl ⊢ J ∈ N-Locally Comp → ⋃ J ∈ J
6 5 adantr ⊢ J ∈ N-Locally Comp ∧ x ∈ ⋃ J → ⋃ J ∈ J
7 simpr ⊢ J ∈ N-Locally Comp ∧ x ∈ ⋃ J → x ∈ ⋃ J
8 nllyi ⊢ J ∈ N-Locally Comp ∧ ⋃ J ∈ J ∧ x ∈ ⋃ J → ∃ k ∈ nei ⁡ J ⁡ x k ⊆ ⋃ J ∧ J ↾ 𝑡 k ∈ Comp
9 3 6 7 8 syl3anc ⊢ J ∈ N-Locally Comp ∧ x ∈ ⋃ J → ∃ k ∈ nei ⁡ J ⁡ x k ⊆ ⋃ J ∧ J ↾ 𝑡 k ∈ Comp
10 simpr ⊢ k ⊆ ⋃ J ∧ J ↾ 𝑡 k ∈ Comp → J ↾ 𝑡 k ∈ Comp
11 10 reximi ⊢ ∃ k ∈ nei ⁡ J ⁡ x k ⊆ ⋃ J ∧ J ↾ 𝑡 k ∈ Comp → ∃ k ∈ nei ⁡ J ⁡ x J ↾ 𝑡 k ∈ Comp
12 9 11 syl ⊢ J ∈ N-Locally Comp ∧ x ∈ ⋃ J → ∃ k ∈ nei ⁡ J ⁡ x J ↾ 𝑡 k ∈ Comp
13 1 2 12 llycmpkgen2 ⊢ J ∈ N-Locally Comp → J ∈ ran ⁡ 𝑘Gen