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\in \mathrm{Fre}\to \mathrm{KQ}\left(J\right)\in \mathrm{Fre}$$

Proof

Step	Hyp	Ref	Expression
1		t1t0	$$⊢J\in \mathrm{Fre}\to J\in \mathrm{Kol2}$$
2		kqhmph	$$⊢J\in \mathrm{Kol2}\leftrightarrow J\simeq \mathrm{KQ}\left(J\right)$$
3	1 2	sylib	$$⊢J\in \mathrm{Fre}\to J\simeq \mathrm{KQ}\left(J\right)$$
4		t1hmph	$$⊢J\simeq \mathrm{KQ}\left(J\right)\to \left(J\in \mathrm{Fre}\to \mathrm{KQ}\left(J\right)\in \mathrm{Fre}\right)$$
5	3 4	mpcom	$$⊢J\in \mathrm{Fre}\to \mathrm{KQ}\left(J\right)\in \mathrm{Fre}$$