Metamath Proof Explorer


Theorem hausnei2

Description: The Hausdorff condition still holds if one considers general neighborhoods instead of open sets. (Contributed by Jeff Hankins, 5-Sep-2009)

Ref Expression
Assertion hausnei2
|- ( J e. ( TopOn ` X ) -> ( J e. Haus <-> A. x e. X A. y e. X ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 ishaus2
 |-  ( J e. ( TopOn ` X ) -> ( J e. Haus <-> A. x e. X A. y e. X ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
2 topontop
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
3 simp1
 |-  ( ( J e. Top /\ m e. J /\ n e. J ) -> J e. Top )
4 simp2
 |-  ( ( J e. Top /\ m e. J /\ n e. J ) -> m e. J )
5 simp1
 |-  ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> x e. m )
6 opnneip
 |-  ( ( J e. Top /\ m e. J /\ x e. m ) -> m e. ( ( nei ` J ) ` { x } ) )
7 3 4 5 6 syl2an3an
 |-  ( ( ( J e. Top /\ m e. J /\ n e. J ) /\ ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) -> m e. ( ( nei ` J ) ` { x } ) )
8 simp3
 |-  ( ( J e. Top /\ m e. J /\ n e. J ) -> n e. J )
9 simp2
 |-  ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> y e. n )
10 opnneip
 |-  ( ( J e. Top /\ n e. J /\ y e. n ) -> n e. ( ( nei ` J ) ` { y } ) )
11 3 8 9 10 syl2an3an
 |-  ( ( ( J e. Top /\ m e. J /\ n e. J ) /\ ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) -> n e. ( ( nei ` J ) ` { y } ) )
12 simpr3
 |-  ( ( ( J e. Top /\ m e. J /\ n e. J ) /\ ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) -> ( m i^i n ) = (/) )
13 ineq1
 |-  ( u = m -> ( u i^i v ) = ( m i^i v ) )
14 13 eqeq1d
 |-  ( u = m -> ( ( u i^i v ) = (/) <-> ( m i^i v ) = (/) ) )
15 ineq2
 |-  ( v = n -> ( m i^i v ) = ( m i^i n ) )
16 15 eqeq1d
 |-  ( v = n -> ( ( m i^i v ) = (/) <-> ( m i^i n ) = (/) ) )
17 14 16 rspc2ev
 |-  ( ( m e. ( ( nei ` J ) ` { x } ) /\ n e. ( ( nei ` J ) ` { y } ) /\ ( m i^i n ) = (/) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) )
18 7 11 12 17 syl3anc
 |-  ( ( ( J e. Top /\ m e. J /\ n e. J ) /\ ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) )
19 18 ex
 |-  ( ( J e. Top /\ m e. J /\ n e. J ) -> ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) )
20 19 3expib
 |-  ( J e. Top -> ( ( m e. J /\ n e. J ) -> ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) )
21 20 rexlimdvv
 |-  ( J e. Top -> ( E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) )
22 neii2
 |-  ( ( J e. Top /\ u e. ( ( nei ` J ) ` { x } ) ) -> E. m e. J ( { x } C_ m /\ m C_ u ) )
23 22 ex
 |-  ( J e. Top -> ( u e. ( ( nei ` J ) ` { x } ) -> E. m e. J ( { x } C_ m /\ m C_ u ) ) )
24 neii2
 |-  ( ( J e. Top /\ v e. ( ( nei ` J ) ` { y } ) ) -> E. n e. J ( { y } C_ n /\ n C_ v ) )
25 24 ex
 |-  ( J e. Top -> ( v e. ( ( nei ` J ) ` { y } ) -> E. n e. J ( { y } C_ n /\ n C_ v ) ) )
26 vex
 |-  x e. _V
27 26 snss
 |-  ( x e. m <-> { x } C_ m )
28 27 anbi1i
 |-  ( ( x e. m /\ m C_ u ) <-> ( { x } C_ m /\ m C_ u ) )
29 vex
 |-  y e. _V
30 29 snss
 |-  ( y e. n <-> { y } C_ n )
31 30 anbi1i
 |-  ( ( y e. n /\ n C_ v ) <-> ( { y } C_ n /\ n C_ v ) )
32 simp1l
 |-  ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) /\ ( u i^i v ) = (/) ) -> x e. m )
33 simp2l
 |-  ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) /\ ( u i^i v ) = (/) ) -> y e. n )
34 ss2in
 |-  ( ( m C_ u /\ n C_ v ) -> ( m i^i n ) C_ ( u i^i v ) )
35 ssn0
 |-  ( ( ( m i^i n ) C_ ( u i^i v ) /\ ( m i^i n ) =/= (/) ) -> ( u i^i v ) =/= (/) )
36 35 ex
 |-  ( ( m i^i n ) C_ ( u i^i v ) -> ( ( m i^i n ) =/= (/) -> ( u i^i v ) =/= (/) ) )
37 36 necon4d
 |-  ( ( m i^i n ) C_ ( u i^i v ) -> ( ( u i^i v ) = (/) -> ( m i^i n ) = (/) ) )
38 34 37 syl
 |-  ( ( m C_ u /\ n C_ v ) -> ( ( u i^i v ) = (/) -> ( m i^i n ) = (/) ) )
39 38 ad2ant2l
 |-  ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) ) -> ( ( u i^i v ) = (/) -> ( m i^i n ) = (/) ) )
40 39 3impia
 |-  ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) /\ ( u i^i v ) = (/) ) -> ( m i^i n ) = (/) )
41 32 33 40 3jca
 |-  ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) /\ ( u i^i v ) = (/) ) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
42 41 3exp
 |-  ( ( x e. m /\ m C_ u ) -> ( ( y e. n /\ n C_ v ) -> ( ( u i^i v ) = (/) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
43 31 42 syl5bir
 |-  ( ( x e. m /\ m C_ u ) -> ( ( { y } C_ n /\ n C_ v ) -> ( ( u i^i v ) = (/) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
44 43 com3r
 |-  ( ( u i^i v ) = (/) -> ( ( x e. m /\ m C_ u ) -> ( ( { y } C_ n /\ n C_ v ) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
45 44 imp
 |-  ( ( ( u i^i v ) = (/) /\ ( x e. m /\ m C_ u ) ) -> ( ( { y } C_ n /\ n C_ v ) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
46 45 3adant1
 |-  ( ( J e. Top /\ ( u i^i v ) = (/) /\ ( x e. m /\ m C_ u ) ) -> ( ( { y } C_ n /\ n C_ v ) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
47 46 reximdv
 |-  ( ( J e. Top /\ ( u i^i v ) = (/) /\ ( x e. m /\ m C_ u ) ) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
48 47 3exp
 |-  ( J e. Top -> ( ( u i^i v ) = (/) -> ( ( x e. m /\ m C_ u ) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) )
49 48 com34
 |-  ( J e. Top -> ( ( u i^i v ) = (/) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> ( ( x e. m /\ m C_ u ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) )
50 49 3imp
 |-  ( ( J e. Top /\ ( u i^i v ) = (/) /\ E. n e. J ( { y } C_ n /\ n C_ v ) ) -> ( ( x e. m /\ m C_ u ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
51 28 50 syl5bir
 |-  ( ( J e. Top /\ ( u i^i v ) = (/) /\ E. n e. J ( { y } C_ n /\ n C_ v ) ) -> ( ( { x } C_ m /\ m C_ u ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
52 51 reximdv
 |-  ( ( J e. Top /\ ( u i^i v ) = (/) /\ E. n e. J ( { y } C_ n /\ n C_ v ) ) -> ( E. m e. J ( { x } C_ m /\ m C_ u ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
53 52 3exp
 |-  ( J e. Top -> ( ( u i^i v ) = (/) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> ( E. m e. J ( { x } C_ m /\ m C_ u ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) )
54 53 com24
 |-  ( J e. Top -> ( E. m e. J ( { x } C_ m /\ m C_ u ) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> ( ( u i^i v ) = (/) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) )
55 54 impd
 |-  ( J e. Top -> ( ( E. m e. J ( { x } C_ m /\ m C_ u ) /\ E. n e. J ( { y } C_ n /\ n C_ v ) ) -> ( ( u i^i v ) = (/) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
56 23 25 55 syl2and
 |-  ( J e. Top -> ( ( u e. ( ( nei ` J ) ` { x } ) /\ v e. ( ( nei ` J ) ` { y } ) ) -> ( ( u i^i v ) = (/) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
57 56 rexlimdvv
 |-  ( J e. Top -> ( E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
58 21 57 impbid
 |-  ( J e. Top -> ( E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) <-> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) )
59 58 imbi2d
 |-  ( J e. Top -> ( ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) <-> ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) )
60 59 2ralbidv
 |-  ( J e. Top -> ( A. x e. X A. y e. X ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) <-> A. x e. X A. y e. X ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) )
61 2 60 syl
 |-  ( J e. ( TopOn ` X ) -> ( A. x e. X A. y e. X ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) <-> A. x e. X A. y e. X ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) )
62 1 61 bitrd
 |-  ( J e. ( TopOn ` X ) -> ( J e. Haus <-> A. x e. X A. y e. X ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) )