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 ( 𝐽 ∈ Haus β†’ ( π‘˜Gen β€˜ 𝐽 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 haustop ⊒ ( 𝐽 ∈ Haus β†’ 𝐽 ∈ Top )
2 toptopon2 ⊒ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn β€˜ βˆͺ 𝐽 ) )
3 1 2 sylib ⊒ ( 𝐽 ∈ Haus β†’ 𝐽 ∈ ( TopOn β€˜ βˆͺ 𝐽 ) )
4 kgentopon ⊒ ( 𝐽 ∈ ( TopOn β€˜ βˆͺ 𝐽 ) β†’ ( π‘˜Gen β€˜ 𝐽 ) ∈ ( TopOn β€˜ βˆͺ 𝐽 ) )
5 3 4 syl ⊒ ( 𝐽 ∈ Haus β†’ ( π‘˜Gen β€˜ 𝐽 ) ∈ ( TopOn β€˜ βˆͺ 𝐽 ) )
6 kgenss ⊒ ( 𝐽 ∈ Top β†’ 𝐽 βŠ† ( π‘˜Gen β€˜ 𝐽 ) )
7 1 6 syl ⊒ ( 𝐽 ∈ Haus β†’ 𝐽 βŠ† ( π‘˜Gen β€˜ 𝐽 ) )
8 eqid ⊒ βˆͺ 𝐽 = βˆͺ 𝐽
9 8 sshaus ⊒ ( ( 𝐽 ∈ Haus ∧ ( π‘˜Gen β€˜ 𝐽 ) ∈ ( TopOn β€˜ βˆͺ 𝐽 ) ∧ 𝐽 βŠ† ( π‘˜Gen β€˜ 𝐽 ) ) β†’ ( π‘˜Gen β€˜ 𝐽 ) ∈ Haus )
10 5 7 9 mpd3an23 ⊒ ( 𝐽 ∈ Haus β†’ ( π‘˜Gen β€˜ 𝐽 ) ∈ Haus )