This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐽 ∈ ran 𝑘Gen ↔ ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 kgentop ⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top )
2 kgenidm ⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )
3 eqimss ⊢ ( ( 𝑘Gen ‘ 𝐽 ) = 𝐽 → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
4 2 3 syl ⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
5 1 4 jca ⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )
6 simpr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
7 kgenss ⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
8 7 adantr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
9 6 8 eqssd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )
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 ∧ 𝐽 ∈ Top ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen )
14 12 13 mpan ⊢ ( 𝐽 ∈ Top → ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen )
15 14 adantr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen )
16 9 15 eqeltrrd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → 𝐽 ∈ ran 𝑘Gen )
17 5 16 impbii ⊢ ( 𝐽 ∈ ran 𝑘Gen ↔ ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )