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 ∈ ran ⁡ 𝑘Gen ↔ J ∈ Top ∧ 𝑘Gen ⁡ J ⊆ J

Proof

Step Hyp Ref Expression
1 kgentop ⊢ J ∈ ran ⁡ 𝑘Gen → J ∈ Top
2 kgenidm ⊢ J ∈ ran ⁡ 𝑘Gen → 𝑘Gen ⁡ J = J
3 eqimss ⊢ 𝑘Gen ⁡ J = J → 𝑘Gen ⁡ J ⊆ J
4 2 3 syl ⊢ J ∈ ran ⁡ 𝑘Gen → 𝑘Gen ⁡ J ⊆ J
5 1 4 jca ⊢ J ∈ ran ⁡ 𝑘Gen → J ∈ Top ∧ 𝑘Gen ⁡ J ⊆ J
6 simpr ⊢ J ∈ Top ∧ 𝑘Gen ⁡ J ⊆ J → 𝑘Gen ⁡ J ⊆ J
7 kgenss ⊢ J ∈ Top → J ⊆ 𝑘Gen ⁡ J
8 7 adantr ⊢ J ∈ Top ∧ 𝑘Gen ⁡ J ⊆ J → J ⊆ 𝑘Gen ⁡ J
9 6 8 eqssd ⊢ J ∈ Top ∧ 𝑘Gen ⁡ J ⊆ J → 𝑘Gen ⁡ J = J
10 kgenf ⊢ 𝑘Gen : Top ⟶ Top
11 ffn ⊢ 𝑘Gen : Top ⟶ Top → 𝑘Gen Fn Top
12 10 11 ax-mp ⊢ 𝑘Gen Fn Top
13 fnfvelrn ⊢ 𝑘Gen Fn Top ∧ J ∈ Top → 𝑘Gen ⁡ J ∈ ran ⁡ 𝑘Gen
14 12 13 mpan ⊢ J ∈ Top → 𝑘Gen ⁡ J ∈ ran ⁡ 𝑘Gen
15 14 adantr ⊢ J ∈ Top ∧ 𝑘Gen ⁡ J ⊆ J → 𝑘Gen ⁡ J ∈ ran ⁡ 𝑘Gen
16 9 15 eqeltrrd ⊢ J ∈ Top ∧ 𝑘Gen ⁡ J ⊆ J → J ∈ ran ⁡ 𝑘Gen
17 5 16 impbii ⊢ J ∈ ran ⁡ 𝑘Gen ↔ J ∈ Top ∧ 𝑘Gen ⁡ J ⊆ J