Theorem sshaus

Description: A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Hypothesis	t1sep.1	⊢ 𝑋 = ∪ 𝐽
Assertion	sshaus	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ Haus )

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	⊢ 𝑋 = ∪ 𝐽
2		haustop	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
3		cnhaus	⊢ ( ( 𝐽 ∈ Haus ∧ ( I ↾ 𝑋 ) : 𝑋 –1-1→ 𝑋 ∧ ( I ↾ 𝑋 ) ∈ ( 𝐾 Cn 𝐽 ) ) → 𝐾 ∈ Haus )
4	1 2 3	sshauslem	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ Haus )