This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sshaus

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

		Ref	Expression
	Hypothesis	t1sep.1	$⊢ X = ⋃ J$
	Assertion	sshaus	$⊢ (J \in Haus \land K \in TopOn (X) \land J \subseteq K) \to K \in Haus$

Step	Hyp	Ref	Expression
1		t1sep.1	$⊢ X = ⋃ J$
2		haustop	$⊢ J \in Haus \to J \in Top$
3		cnhaus	$⊢ (J \in Haus \land ({I ↾}_{X}) : X \underset{1-1}{⟶} X \land {I ↾}_{X} \in (K Cn J)) \to K \in Haus$
4	1 2 3	sshauslem	$⊢ (J \in Haus \land K \in TopOn (X) \land J \subseteq K) \to K \in Haus$