# 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}\in N-Locally\mathrm{Comp}\to {J}\in \mathrm{ran}\mathrm{𝑘Gen}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\bigcup {J}=\bigcup {J}$
2 nllytop ${⊢}{J}\in N-Locally\mathrm{Comp}\to {J}\in \mathrm{Top}$
3 simpl ${⊢}\left({J}\in N-Locally\mathrm{Comp}\wedge {x}\in \bigcup {J}\to {J}\in N-Locally\mathrm{Comp}\right)$
4 1 topopn ${⊢}{J}\in \mathrm{Top}\to \bigcup {J}\in {J}$
5 2 4 syl ${⊢}{J}\in N-Locally\mathrm{Comp}\to \bigcup {J}\in {J}$
6 5 adantr ${⊢}\left({J}\in N-Locally\mathrm{Comp}\wedge {x}\in \bigcup {J}\to \bigcup {J}\in {J}\right)$
7 simpr ${⊢}\left({J}\in N-Locally\mathrm{Comp}\wedge {x}\in \bigcup {J}\to {x}\in \bigcup {J}\right)$
8 nllyi ${⊢}\left({J}\in N-Locally\mathrm{Comp}\wedge \bigcup {J}\in {J}\wedge {x}\in \bigcup {J}\to \exists {k}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}\right)$
9 3 6 7 8 syl3anc ${⊢}\left({J}\in N-Locally\mathrm{Comp}\wedge {x}\in \bigcup {J}\to \exists {k}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}\right)$
10 simpr ${⊢}\left({k}\subseteq \bigcup {J}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{Comp}$
11 10 reximi ${⊢}\exists {k}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({k}\subseteq \bigcup {J}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \exists {k}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{J}{↾}_{𝑡}{k}\in \mathrm{Comp}$
12 9 11 syl ${⊢}\left({J}\in N-Locally\mathrm{Comp}\wedge {x}\in \bigcup {J}\to \exists {k}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}\right)$
13 1 2 12 llycmpkgen2 ${⊢}{J}\in N-Locally\mathrm{Comp}\to {J}\in \mathrm{ran}\mathrm{𝑘Gen}$