Theorem ist1-5

Description: A topological space is T_1 iff it is both T_0 and R_0. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	ist1-5	$$⊢J\in \mathrm{Fre}\leftrightarrow \left(J\in \mathrm{Kol2}\wedge \mathrm{KQ}\left(J\right)\in \mathrm{Fre}\right)$$

Proof

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