Metamath Proof Explorer


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 Fre KQ J Fre

Proof

Step Hyp Ref Expression
1 t1t0 J Fre J Kol2
2 kqhmph J Kol2 J KQ J
3 1 2 sylib J Fre J KQ J
4 t1hmph J KQ J J Fre KQ J Fre
5 3 4 mpcom J Fre KQ J Fre