# Metamath Proof Explorer

## Theorem iskgen2

Description: A space is compactly generated iff it contains its image under the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion iskgen2 ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}↔\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)$

### Proof

Step Hyp Ref Expression
1 kgentop ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to {J}\in \mathrm{Top}$
2 kgenidm ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to \mathrm{𝑘Gen}\left({J}\right)={J}$
3 eqimss ${⊢}\mathrm{𝑘Gen}\left({J}\right)={J}\to \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}$
4 2 3 syl ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}$
5 1 4 jca ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}\to \left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)$
6 simpr ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)\to \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}$
7 kgenss ${⊢}{J}\in \mathrm{Top}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
8 7 adantr ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
9 6 8 eqssd ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)\to \mathrm{𝑘Gen}\left({J}\right)={J}$
10 kgenf ${⊢}\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}$
11 ffn ${⊢}\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}\to \mathrm{𝑘Gen}Fn\mathrm{Top}$
12 10 11 ax-mp ${⊢}\mathrm{𝑘Gen}Fn\mathrm{Top}$
13 fnfvelrn ${⊢}\left(\mathrm{𝑘Gen}Fn\mathrm{Top}\wedge {J}\in \mathrm{Top}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{ran}\mathrm{𝑘Gen}$
14 12 13 mpan ${⊢}{J}\in \mathrm{Top}\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{ran}\mathrm{𝑘Gen}$
15 14 adantr ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{ran}\mathrm{𝑘Gen}$
16 9 15 eqeltrrd ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)\to {J}\in \mathrm{ran}\mathrm{𝑘Gen}$
17 5 16 impbii ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}↔\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)$