This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step	Hyp	Ref	Expression
1		t1t0	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Kol2 )
2		kqhmph	⊢ ( 𝐽 ∈ Kol2 ↔ 𝐽 ≃ ( KQ ‘ 𝐽 ) )
3	1 2	sylib	⊢ ( 𝐽 ∈ Fre → 𝐽 ≃ ( KQ ‘ 𝐽 ) )
4		t1hmph	⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → ( 𝐽 ∈ Fre → ( KQ ‘ 𝐽 ) ∈ Fre ) )
5	3 4	mpcom	⊢ ( 𝐽 ∈ Fre → ( KQ ‘ 𝐽 ) ∈ Fre )