# Metamath Proof Explorer

## Theorem cmpkgen

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

Ref Expression
Assertion cmpkgen ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{ran}\mathrm{𝑘Gen}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\bigcup {J}=\bigcup {J}$
2 cmptop ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{Top}$
3 2 adantr ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to {J}\in \mathrm{Top}$
4 1 topopn ${⊢}{J}\in \mathrm{Top}\to \bigcup {J}\in {J}$
5 3 4 syl ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to \bigcup {J}\in {J}$
6 simpr ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to {x}\in \bigcup {J}$
7 6 snssd ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to \left\{{x}\right\}\subseteq \bigcup {J}$
8 opnneiss ${⊢}\left({J}\in \mathrm{Top}\wedge \bigcup {J}\in {J}\wedge \left\{{x}\right\}\subseteq \bigcup {J}\right)\to \bigcup {J}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)$
9 3 5 7 8 syl3anc ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to \bigcup {J}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)$
10 1 restid ${⊢}{J}\in \mathrm{Top}\to {J}{↾}_{𝑡}\bigcup {J}={J}$
11 3 10 syl ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to {J}{↾}_{𝑡}\bigcup {J}={J}$
12 simpl ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to {J}\in \mathrm{Comp}$
13 11 12 eqeltrd ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to {J}{↾}_{𝑡}\bigcup {J}\in \mathrm{Comp}$
14 oveq2 ${⊢}{k}=\bigcup {J}\to {J}{↾}_{𝑡}{k}={J}{↾}_{𝑡}\bigcup {J}$
15 14 eleq1d ${⊢}{k}=\bigcup {J}\to \left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}↔{J}{↾}_{𝑡}\bigcup {J}\in \mathrm{Comp}\right)$
16 15 rspcev ${⊢}\left(\bigcup {J}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\wedge {J}{↾}_{𝑡}\bigcup {J}\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}$
17 9 13 16 syl2anc ${⊢}\left({J}\in \mathrm{Comp}\wedge {x}\in \bigcup {J}\right)\to \exists {k}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{J}{↾}_{𝑡}{k}\in \mathrm{Comp}$
18 1 2 17 llycmpkgen2 ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{ran}\mathrm{𝑘Gen}$