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

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 e. Haus -> ( kGen ` J ) e. Haus )

Proof

Step Hyp Ref Expression
1 haustop 
 |-  ( J e. Haus -> J e. Top )
2 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
3 1 2 sylib 
 |-  ( J e. Haus -> J e. ( TopOn ` U. J ) )
4 kgentopon 
 |-  ( J e. ( TopOn ` U. J ) -> ( kGen ` J ) e. ( TopOn ` U. J ) )
5 3 4 syl 
 |-  ( J e. Haus -> ( kGen ` J ) e. ( TopOn ` U. J ) )
6 kgenss 
 |-  ( J e. Top -> J C_ ( kGen ` J ) )
7 1 6 syl 
 |-  ( J e. Haus -> J C_ ( kGen ` J ) )
8 eqid 
 |-  U. J = U. J
9 8 sshaus 
 |-  ( ( J e. Haus /\ ( kGen ` J ) e. ( TopOn ` U. J ) /\ J C_ ( kGen ` J ) ) -> ( kGen ` J ) e. Haus )
10 5 7 9 mpd3an23 
 |-  ( J e. Haus -> ( kGen ` J ) e. Haus )