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 )