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 )