Metamath Proof Explorer

Theorem kgenhaus

Description: The compact generator generates another Hausdorff topology given a Hausdorff topology to start from. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgenhaus ⊢ J ∈ Haus → 𝑘Gen ⁡ J ∈ Haus

Proof

Step Hyp Ref Expression
1 haustop ⊢ J ∈ Haus → J ∈ Top
2 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
3 1 2 sylib ⊢ J ∈ Haus → J ∈ TopOn ⁡ ⋃ J
4 kgentopon ⊢ J ∈ TopOn ⁡ ⋃ J → 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J
5 3 4 syl ⊢ J ∈ Haus → 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J
6 kgenss ⊢ J ∈ Top → J ⊆ 𝑘Gen ⁡ J
7 1 6 syl ⊢ J ∈ Haus → J ⊆ 𝑘Gen ⁡ J
8 eqid ⊢ ⋃ J = ⋃ J
9 8 sshaus ⊢ J ∈ Haus ∧ 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J ∧ J ⊆ 𝑘Gen ⁡ J → 𝑘Gen ⁡ J ∈ Haus
10 5 7 9 mpd3an23 ⊢ J ∈ Haus → 𝑘Gen ⁡ J ∈ Haus