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 = ⋃ J$
	Assertion	sst0	$⊢ (J \in Kol2 \land K \in TopOn (X) \land J \subseteq K) \to K \in Kol2$

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