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

Metamath Proof Explorer

Theorem haushmph

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

		Ref	Expression
	Assertion	haushmph	$⊢ J ≃ K \to (J \in Haus \to K \in Haus)$

Step	Hyp	Ref	Expression
1		haustop	$⊢ J \in Haus \to J \in Top$
2		cnhaus	$⊢ (J \in Haus \land f : ⋃ K \underset{1-1}{⟶} ⋃ J \land f \in (K Cn J)) \to K \in Haus$
3	1 2	haushmphlem	$⊢ J ≃ K \to (J \in Haus \to K \in Haus)$