Theorem hausnei

Description: Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007)

	Ref	Expression
Hypothesis	ist0.1	|- X = U. J
Assertion	hausnei	|- ( ( J e. Haus /\ ( P e. X /\ Q e. X /\ P =/= Q ) ) -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		ist0.1	|- X = U. J
2	1	ishaus	|- ( J e. Haus <-> ( J e. Top /\ A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) )
3	2	simprbi	|- ( J e. Haus -> A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) )
4		neeq1	|- ( x = P -> ( x =/= y <-> P =/= y ) )
5		eleq1	|- ( x = P -> ( x e. n <-> P e. n ) )
6	5	3anbi1d	|- ( x = P -> ( ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) )
7	6	2rexbidv	|- ( x = P -> ( E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> E. n e. J E. m e. J ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) )
8	4 7	imbi12d	|- ( x = P -> ( ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) <-> ( P =/= y -> E. n e. J E. m e. J ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) )
9		neeq2	|- ( y = Q -> ( P =/= y <-> P =/= Q ) )
10		eleq1	|- ( y = Q -> ( y e. m <-> Q e. m ) )
11	10	3anbi2d	|- ( y = Q -> ( ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) )
12	11	2rexbidv	|- ( y = Q -> ( E. n e. J E. m e. J ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) )
13	9 12	imbi12d	|- ( y = Q -> ( ( P =/= y -> E. n e. J E. m e. J ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) <-> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) )
14	8 13	rspc2v	|- ( ( P e. X /\ Q e. X ) -> ( A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) -> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) )
15	3 14	syl5	|- ( ( P e. X /\ Q e. X ) -> ( J e. Haus -> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) )
16	15	ex	|- ( P e. X -> ( Q e. X -> ( J e. Haus -> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) ) )
17	16	com3r	|- ( J e. Haus -> ( P e. X -> ( Q e. X -> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) ) )
18	17	3imp2	|- ( ( J e. Haus /\ ( P e. X /\ Q e. X /\ P =/= Q ) ) -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) )