Theorem t0hmph

Description: T_0 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	t0hmph	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Kol2 → 𝐾 ∈ Kol2 ) )

Proof

Step	Hyp	Ref	Expression
1		t0top	⊢ ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top )
2		cnt0	⊢ ( ( 𝐽 ∈ Kol2 ∧ 𝑓 : ∪ 𝐾 –1-1→ ∪ 𝐽 ∧ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ) → 𝐾 ∈ Kol2 )
3	1 2	haushmphlem	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Kol2 → 𝐾 ∈ Kol2 ) )