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 = U. J
Assertion	sshaus	|- ( ( J e. Haus /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. Haus )

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	|- X = U. J
2		haustop	|- ( J e. Haus -> J e. Top )
3		cnhaus	|- ( ( J e. Haus /\ ( _I |` X ) : X -1-1-> X /\ ( _I |` X ) e. ( K Cn J ) ) -> K e. Haus )
4	1 2 3	sshauslem	|- ( ( J e. Haus /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. Haus )