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 e. N-Locally 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	2	restnlly	|- ( T. -> N-Locally Haus = Locally Haus )
4	3	mptru	|- N-Locally Haus = Locally Haus
5	4	eleq2i	|- ( J e. N-Locally Haus <-> J e. Locally Haus )