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 ) = (/) ) ) )