Metamath Proof Explorer

Theorem kgenftop

Description: The compact generator generates a topology. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenftop ⊢ J ∈ Top → 𝑘Gen ⁡ J ∈ Top

Proof

Step Hyp Ref Expression
1 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
2 kgentopon ⊢ J ∈ TopOn ⁡ ⋃ J → 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J
3 1 2 sylbi ⊢ J ∈ Top → 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J
4 topontop ⊢ 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J → 𝑘Gen ⁡ J ∈ Top
5 3 4 syl ⊢ J ∈ Top → 𝑘Gen ⁡ J ∈ Top