Metamath Proof Explorer

Theorem hausflim

Description: A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flimcf.1 
|- X = U. J
Assertion hausflim 
|- ( J e. Haus <-> ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) )

Proof

Step Hyp Ref Expression
1 flimcf.1 
 |-  X = U. J
2 haustop 
 |-  ( J e. Haus -> J e. Top )
3 hausflimi 
 |-  ( J e. Haus -> E* x x e. ( J fLim f ) )
4 3 ralrimivw 
 |-  ( J e. Haus -> A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) )
5 2 4 jca 
 |-  ( J e. Haus -> ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) )
6 simpl 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> J e. Top )
7 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
8 6 7 sylib 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> J e. ( TopOn ` X ) )
9 simprll 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> z e. X )
10 9 snssd 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> { z } C_ X )
11 snnzg 
 |-  ( z e. X -> { z } =/= (/) )
12 9 11 syl 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> { z } =/= (/) )
13 neifil 
 |-  ( ( J e. ( TopOn ` X ) /\ { z } C_ X /\ { z } =/= (/) ) -> ( ( nei ` J ) ` { z } ) e. ( Fil ` X ) )
14 8 10 12 13 syl3anc 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( nei ` J ) ` { z } ) e. ( Fil ` X ) )
15 filfbas 
 |-  ( ( ( nei ` J ) ` { z } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { z } ) e. ( fBas ` X ) )
16 14 15 syl 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( nei ` J ) ` { z } ) e. ( fBas ` X ) )
17 simprlr 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> w e. X )
18 17 snssd 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> { w } C_ X )
19 snnzg 
 |-  ( w e. X -> { w } =/= (/) )
20 17 19 syl 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> { w } =/= (/) )
21 neifil 
 |-  ( ( J e. ( TopOn ` X ) /\ { w } C_ X /\ { w } =/= (/) ) -> ( ( nei ` J ) ` { w } ) e. ( Fil ` X ) )
22 8 18 20 21 syl3anc 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( nei ` J ) ` { w } ) e. ( Fil ` X ) )
23 filfbas 
 |-  ( ( ( nei ` J ) ` { w } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { w } ) e. ( fBas ` X ) )
24 22 23 syl 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( nei ` J ) ` { w } ) e. ( fBas ` X ) )
25 fbunfip 
 |-  ( ( ( ( nei ` J ) ` { z } ) e. ( fBas ` X ) /\ ( ( nei ` J ) ` { w } ) e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) <-> A. u e. ( ( nei ` J ) ` { z } ) A. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) =/= (/) ) )
26 16 24 25 syl2anc 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) <-> A. u e. ( ( nei ` J ) ` { z } ) A. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) =/= (/) ) )
27 1 neisspw 
 |-  ( J e. Top -> ( ( nei ` J ) ` { z } ) C_ ~P X )
28 1 neisspw 
 |-  ( J e. Top -> ( ( nei ` J ) ` { w } ) C_ ~P X )
29 27 28 unssd 
 |-  ( J e. Top -> ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ~P X )
30 29 adantr 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ~P X )
31 30 a1d 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) -> ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ~P X ) )
32 ssun1 
 |-  ( ( nei ` J ) ` { z } ) C_ ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) )
33 filn0 
 |-  ( ( ( nei ` J ) ` { z } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { z } ) =/= (/) )
34 14 33 syl 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( nei ` J ) ` { z } ) =/= (/) )
35 ssn0 
 |-  ( ( ( ( nei ` J ) ` { z } ) C_ ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) /\ ( ( nei ` J ) ` { z } ) =/= (/) ) -> ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) =/= (/) )
36 32 34 35 sylancr 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) =/= (/) )
37 36 a1d 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) -> ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) =/= (/) ) )
38 idd 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) -> -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) )
39 31 37 38 3jcad 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) -> ( ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ~P X /\ ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) =/= (/) /\ -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) )
40 1 topopn 
 |-  ( J e. Top -> X e. J )
41 40 adantr 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> X e. J )
42 fsubbas 
 |-  ( X e. J -> ( ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) <-> ( ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ~P X /\ ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) =/= (/) /\ -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) )
43 41 42 syl 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) <-> ( ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ~P X /\ ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) =/= (/) /\ -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) )
44 fgcl 
 |-  ( ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) e. ( Fil ` X ) )
45 44 adantl 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) e. ( Fil ` X ) )
46 simplrr 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> z =/= w )
47 9 adantr 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> z e. X )
48 17 adantr 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> w e. X )
49 fvex 
 |-  ( ( nei ` J ) ` { z } ) e. _V
50 fvex 
 |-  ( ( nei ` J ) ` { w } ) e. _V
51 49 50 unex 
 |-  ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) e. _V
52 ssfii 
 |-  ( ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) e. _V -> ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) )
53 51 52 ax-mp 
 |-  ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) )
54 ssfg 
 |-  ( ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) -> ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) )
55 54 adantl 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) )
56 53 55 sstrid 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) )
57 32 56 sstrid 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( ( nei ` J ) ` { z } ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) )
58 8 adantr 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> J e. ( TopOn ` X ) )
59 elflim 
 |-  ( ( J e. ( TopOn ` X ) /\ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) e. ( Fil ` X ) ) -> ( z e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) <-> ( z e. X /\ ( ( nei ` J ) ` { z } ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
60 58 45 59 syl2anc 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( z e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) <-> ( z e. X /\ ( ( nei ` J ) ` { z } ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
61 47 57 60 mpbir2and 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> z e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) )
62 56 unssbd 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( ( nei ` J ) ` { w } ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) )
63 elflim 
 |-  ( ( J e. ( TopOn ` X ) /\ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) e. ( Fil ` X ) ) -> ( w e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) <-> ( w e. X /\ ( ( nei ` J ) ` { w } ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
64 58 45 63 syl2anc 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( w e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) <-> ( w e. X /\ ( ( nei ` J ) ` { w } ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
65 48 62 64 mpbir2and 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> w e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) )
66 eleq1w 
 |-  ( x = z -> ( x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) <-> z e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
67 eleq1w 
 |-  ( x = w -> ( x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) <-> w e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
68 66 67 moi 
 |-  ( ( ( z e. X /\ w e. X ) /\ E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) /\ ( z e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) /\ w e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) ) -> z = w )
69 68 3com23 
 |-  ( ( ( z e. X /\ w e. X ) /\ ( z e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) /\ w e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) /\ E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) -> z = w )
70 69 3expia 
 |-  ( ( ( z e. X /\ w e. X ) /\ ( z e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) /\ w e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) ) -> ( E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) -> z = w ) )
71 47 48 61 65 70 syl22anc 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) -> z = w ) )
72 71 necon3ad 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> ( z =/= w -> -. E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
73 46 72 mpd 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> -. E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) )
74 oveq2 
 |-  ( f = ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) -> ( J fLim f ) = ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) )
75 74 eleq2d 
 |-  ( f = ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) -> ( x e. ( J fLim f ) <-> x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
76 75 mobidv 
 |-  ( f = ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) -> ( E* x x e. ( J fLim f ) <-> E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
77 76 notbid 
 |-  ( f = ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) -> ( -. E* x x e. ( J fLim f ) <-> -. E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) )
78 77 rspcev 
 |-  ( ( ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) e. ( Fil ` X ) /\ -. E* x x e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) ) ) -> E. f e. ( Fil ` X ) -. E* x x e. ( J fLim f ) )
79 45 73 78 syl2anc 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) ) -> E. f e. ( Fil ` X ) -. E* x x e. ( J fLim f ) )
80 79 ex 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) e. ( fBas ` X ) -> E. f e. ( Fil ` X ) -. E* x x e. ( J fLim f ) ) )
81 43 80 sylbird 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( ( ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) C_ ~P X /\ ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) =/= (/) /\ -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) ) -> E. f e. ( Fil ` X ) -. E* x x e. ( J fLim f ) ) )
82 39 81 syld 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { z } ) u. ( ( nei ` J ) ` { w } ) ) ) -> E. f e. ( Fil ` X ) -. E* x x e. ( J fLim f ) ) )
83 26 82 sylbird 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( A. u e. ( ( nei ` J ) ` { z } ) A. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) =/= (/) -> E. f e. ( Fil ` X ) -. E* x x e. ( J fLim f ) ) )
84 df-ne 
 |-  ( ( u i^i v ) =/= (/) <-> -. ( u i^i v ) = (/) )
85 84 ralbii 
 |-  ( A. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) =/= (/) <-> A. v e. ( ( nei ` J ) ` { w } ) -. ( u i^i v ) = (/) )
86 ralnex 
 |-  ( A. v e. ( ( nei ` J ) ` { w } ) -. ( u i^i v ) = (/) <-> -. E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) )
87 85 86 bitri 
 |-  ( A. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) =/= (/) <-> -. E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) )
88 87 ralbii 
 |-  ( A. u e. ( ( nei ` J ) ` { z } ) A. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) =/= (/) <-> A. u e. ( ( nei ` J ) ` { z } ) -. E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) )
89 ralnex 
 |-  ( A. u e. ( ( nei ` J ) ` { z } ) -. E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) <-> -. E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) )
90 88 89 bitri 
 |-  ( A. u e. ( ( nei ` J ) ` { z } ) A. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) =/= (/) <-> -. E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) )
91 rexnal 
 |-  ( E. f e. ( Fil ` X ) -. E* x x e. ( J fLim f ) <-> -. A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) )
92 83 90 91 3imtr3g 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( -. E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) -> -. A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) )
93 92 con4d 
 |-  ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> ( A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) -> E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) ) )
94 93 imp 
 |-  ( ( ( J e. Top /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) -> E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) )
95 94 an32s 
 |-  ( ( ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) /\ ( ( z e. X /\ w e. X ) /\ z =/= w ) ) -> E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) )
96 95 expr 
 |-  ( ( ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) /\ ( z e. X /\ w e. X ) ) -> ( z =/= w -> E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) ) )
97 96 ralrimivva 
 |-  ( ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) -> A. z e. X A. w e. X ( z =/= w -> E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) ) )
98 simpl 
 |-  ( ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) -> J e. Top )
99 98 7 sylib 
 |-  ( ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) -> J e. ( TopOn ` X ) )
100 hausnei2 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Haus <-> A. z e. X A. w e. X ( z =/= w -> E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) ) ) )
101 99 100 syl 
 |-  ( ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) -> ( J e. Haus <-> A. z e. X A. w e. X ( z =/= w -> E. u e. ( ( nei ` J ) ` { z } ) E. v e. ( ( nei ` J ) ` { w } ) ( u i^i v ) = (/) ) ) )
102 97 101 mpbird 
 |-  ( ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) -> J e. Haus )
103 5 102 impbii 
 |-  ( J e. Haus <-> ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) )