Metamath Proof Explorer

Theorem hausnlly

Description: A Hausdorff space is n-locally Hausdorff iff it is locally Hausdorff (both notions are thus referred to as "locally Hausdorff"). (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	hausnlly	$⊢ J \in N-LocallyHaus\leftrightarrowJ \in LocallyHaus$

Proof

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	2	restnlly	$⊢ ⊤ \to N-LocallyHaus=LocallyHaus$
4	3	mptru	$⊢ N-LocallyHaus=LocallyHaus$
5	4	eleq2i	$⊢ J \in N-LocallyHaus\leftrightarrowJ \in LocallyHaus$