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


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