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 )