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	⊢ ( 𝐽 ∈ 𝑛-Locally Haus ↔ 𝐽 ∈ Locally Haus )

Proof

Step	Hyp	Ref	Expression
1		resthaus	⊢ ( ( 𝑗 ∈ Haus ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ Haus )
2	1	adantl	⊢ ( ( ⊤ ∧ ( 𝑗 ∈ Haus ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ Haus )
3	2	restnlly	⊢ ( ⊤ → 𝑛-Locally Haus = Locally Haus )
4	3	mptru	⊢ 𝑛-Locally Haus = Locally Haus
5	4	eleq2i	⊢ ( 𝐽 ∈ 𝑛-Locally Haus ↔ 𝐽 ∈ Locally Haus )