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β†’π‘˜GenFnTop
12 10 11 ax-mp βŠ’π‘˜GenFnTop
13 fnfvelrn βŠ’π‘˜GenFnTop∧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