Theorem hauslly

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

	Ref	Expression
Assertion	hauslly	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Locally Haus )

Proof

Step	Hyp	Ref	Expression
1		resthaus	⊢ ( ( 𝑗 ∈ Haus ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ Haus )
2	1	adantl	⊢ ( ( ⊤ ∧ ( 𝑗 ∈ Haus ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ Haus )
3		haustop	⊢ ( 𝑗 ∈ Haus → 𝑗 ∈ Top )
4	3	ssriv	⊢ Haus ⊆ Top
5	4	a1i	⊢ ( ⊤ → Haus ⊆ Top )
6	2 5	restlly	⊢ ( ⊤ → Haus ⊆ Locally Haus )
7	6	mptru	⊢ Haus ⊆ Locally Haus
8	7	sseli	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Locally Haus )