Theorem sst1

Description: A topology finer than a T_1 topology is T_1. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	t1sep.1	|- X = U. J
Assertion	sst1	|- ( ( J e. Fre /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. Fre )

Proof

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