Theorem hauslly

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

	Ref	Expression
Assertion	hauslly	|- ( J e. Haus -> J e. Locally Haus )

Proof

Step	Hyp	Ref	Expression
1		resthaus	|- ( ( j e. Haus /\ x e. j ) -> ( j |`t x ) e. Haus )
2	1	adantl	|- ( ( T. /\ ( j e. Haus /\ x e. j ) ) -> ( j |`t x ) e. Haus )
3		haustop	|- ( j e. Haus -> j e. Top )
4	3	ssriv	|- Haus C_ Top
5	4	a1i	|- ( T. -> Haus C_ Top )
6	2 5	restlly	|- ( T. -> Haus C_ Locally Haus )
7	6	mptru	|- Haus C_ Locally Haus
8	7	sseli	|- ( J e. Haus -> J e. Locally Haus )