Theorem ishaus3

Description: A topological space is Hausdorff iff it is both T_0 and R_1 (where R_1 means that any two topologically distinct points are separated by neighborhoods). (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	ishaus3	⊢ ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ Haus ) )

Proof

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