hauslly

Description: A Hausdorff space is locally Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	hauslly	$⊢ J \in Haus \to J \in LocallyHaus$

Step	Hyp	Ref	Expression
1		resthaus	$⊢ (j \in Haus \land x \in j) \to j ↾_{𝑡} x \in Haus$
2	1	adantl	$⊢ (⊤ \land (j \in Haus \land x \in j)) \to j ↾_{𝑡} x \in Haus$
3		haustop	$⊢ j \in Haus \to j \in Top$
4	3	ssriv	$⊢ Haus \subseteq Top$
5	4	a1i	$⊢ ⊤ \to Haus \subseteq Top$
6	2 5	restlly	$⊢ ⊤ \to Haus \subseteq LocallyHaus$
7	6	mptru	$⊢ Haus \subseteq LocallyHaus$
8	7	sseli	$⊢ J \in Haus \to J \in LocallyHaus$

Metamath Proof Explorer