Theorem t1r0

Description: A T_1 space is R_0. That is, the Kolmogorov quotient of a T_1 space is also T_1 (because they are homeomorphic). (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	t1r0	|- ( J e. Fre -> ( KQ ` J ) e. Fre )

Proof

Step	Hyp	Ref	Expression
1		t1t0	|- ( J e. Fre -> J e. Kol2 )
2		kqhmph	|- ( J e. Kol2 <-> J ~= ( KQ ` J ) )
3	1 2	sylib	|- ( J e. Fre -> J ~= ( KQ ` J ) )
4		t1hmph	|- ( J ~= ( KQ ` J ) -> ( J e. Fre -> ( KQ ` J ) e. Fre ) )
5	3 4	mpcom	|- ( J e. Fre -> ( KQ ` J ) e. Fre )