# 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}\in \mathrm{Haus}\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Haus}$

### Proof

Step Hyp Ref Expression
1 haustop ${⊢}{J}\in \mathrm{Haus}\to {J}\in \mathrm{Top}$
2 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
3 1 2 sylib ${⊢}{J}\in \mathrm{Haus}\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
4 kgentopon ${⊢}{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left(\bigcup {J}\right)$
5 3 4 syl ${⊢}{J}\in \mathrm{Haus}\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left(\bigcup {J}\right)$
6 kgenss ${⊢}{J}\in \mathrm{Top}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
7 1 6 syl ${⊢}{J}\in \mathrm{Haus}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
8 eqid ${⊢}\bigcup {J}=\bigcup {J}$
9 8 sshaus ${⊢}\left({J}\in \mathrm{Haus}\wedge \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left(\bigcup {J}\right)\wedge {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Haus}$
10 5 7 9 mpd3an23 ${⊢}{J}\in \mathrm{Haus}\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Haus}$