Theorem t1hmph

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

	Ref	Expression
Assertion	t1hmph	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Fre → 𝐾 ∈ Fre ) )

Proof

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