This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem llycmpkgen

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

Ref Expression
Assertion llycmpkgen ( 𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ ran 𝑘Gen )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 nllytop ⊢ ( 𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ Top )
3 simpl ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐽 ∈ 𝑛-Locally Comp )
4 1 topopn ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 )
5 2 4 syl ⊢ ( 𝐽 ∈ 𝑛-Locally Comp → ∪ 𝐽 ∈ 𝐽 )
6 5 adantr ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → ∪ 𝐽 ∈ 𝐽 )
7 simpr ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝑥 ∈ ∪ 𝐽 )
8 nllyi ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ ∪ 𝐽 ∈ 𝐽 ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑘 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑘 ⊆ ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) )
9 3 6 7 8 syl3anc ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑘 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑘 ⊆ ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) )
10 simpr ⊢ ( ( 𝑘 ⊆ ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) → ( 𝐽 ↾t 𝑘 ) ∈ Comp )
11 10 reximi ⊢ ( ∃ 𝑘 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑘 ⊆ ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) → ∃ 𝑘 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝐽 ↾t 𝑘 ) ∈ Comp )
12 9 11 syl ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑘 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝐽 ↾t 𝑘 ) ∈ Comp )
13 1 2 12 llycmpkgen2 ⊢ ( 𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ ran 𝑘Gen )