Theorem haushmph

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

	Ref	Expression
Assertion	haushmph	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Haus → 𝐾 ∈ Haus ) )

Proof

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