Metamath Proof Explorer

Theorem sst0

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

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

Proof

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