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	⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) )

Proof

Step	Hyp	Ref	Expression
1		t1t0	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Kol2 )
2		t1hmph	⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → ( 𝐽 ∈ Fre → ( KQ ‘ 𝐽 ) ∈ Fre ) )
3		t1hmph	⊢ ( ( KQ ‘ 𝐽 ) ≃ 𝐽 → ( ( KQ ‘ 𝐽 ) ∈ Fre → 𝐽 ∈ Fre ) )
4	1 2 3	ist1-5lem	⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) )