Metamath Proof Explorer


Theorem fclsfnflim

Description: A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion fclsfnflim FFilXAJfClusFgFilXFgAJfLimg

Proof

Step Hyp Ref Expression
1 filsspw FFilXF𝒫X
2 1 adantr FFilXAJfClusFF𝒫X
3 fclstop AJfClusFJTop
4 3 adantl FFilXAJfClusFJTop
5 eqid J=J
6 5 neisspw JTopneiJA𝒫J
7 4 6 syl FFilXAJfClusFneiJA𝒫J
8 filunibas FFilXF=X
9 5 fclsfil AJfClusFFFilJ
10 filunibas FFilJF=J
11 9 10 syl AJfClusFF=J
12 8 11 sylan9req FFilXAJfClusFX=J
13 12 pweqd FFilXAJfClusF𝒫X=𝒫J
14 7 13 sseqtrrd FFilXAJfClusFneiJA𝒫X
15 2 14 unssd FFilXAJfClusFFneiJA𝒫X
16 ssun1 FFneiJA
17 filn0 FFilXF
18 ssn0 FFneiJAFFneiJA
19 16 17 18 sylancr FFilXFneiJA
20 19 adantr FFilXAJfClusFFneiJA
21 incom yx=xy
22 fclsneii AJfClusFyneiJAxFyx
23 21 22 eqnetrrid AJfClusFyneiJAxFxy
24 23 3com23 AJfClusFxFyneiJAxy
25 24 3expb AJfClusFxFyneiJAxy
26 25 adantll FFilXAJfClusFxFyneiJAxy
27 26 ralrimivva FFilXAJfClusFxFyneiJAxy
28 filfbas FFilXFfBasX
29 28 adantr FFilXAJfClusFFfBasX
30 istopon JTopOnXJTopX=J
31 4 12 30 sylanbrc FFilXAJfClusFJTopOnX
32 5 fclselbas AJfClusFAJ
33 32 adantl FFilXAJfClusFAJ
34 33 12 eleqtrrd FFilXAJfClusFAX
35 34 snssd FFilXAJfClusFAX
36 snnzg AJfClusFA
37 36 adantl FFilXAJfClusFA
38 neifil JTopOnXAXAneiJAFilX
39 31 35 37 38 syl3anc FFilXAJfClusFneiJAFilX
40 filfbas neiJAFilXneiJAfBasX
41 39 40 syl FFilXAJfClusFneiJAfBasX
42 fbunfip FfBasXneiJAfBasX¬fiFneiJAxFyneiJAxy
43 29 41 42 syl2anc FFilXAJfClusF¬fiFneiJAxFyneiJAxy
44 27 43 mpbird FFilXAJfClusF¬fiFneiJA
45 filtop FFilXXF
46 fsubbas XFfiFneiJAfBasXFneiJA𝒫XFneiJA¬fiFneiJA
47 45 46 syl FFilXfiFneiJAfBasXFneiJA𝒫XFneiJA¬fiFneiJA
48 47 adantr FFilXAJfClusFfiFneiJAfBasXFneiJA𝒫XFneiJA¬fiFneiJA
49 15 20 44 48 mpbir3and FFilXAJfClusFfiFneiJAfBasX
50 fgcl fiFneiJAfBasXXfilGenfiFneiJAFilX
51 49 50 syl FFilXAJfClusFXfilGenfiFneiJAFilX
52 fvex neiJAV
53 unexg FFilXneiJAVFneiJAV
54 52 53 mpan2 FFilXFneiJAV
55 ssfii FneiJAVFneiJAfiFneiJA
56 54 55 syl FFilXFneiJAfiFneiJA
57 56 adantr FFilXAJfClusFFneiJAfiFneiJA
58 57 unssad FFilXAJfClusFFfiFneiJA
59 ssfg fiFneiJAfBasXfiFneiJAXfilGenfiFneiJA
60 49 59 syl FFilXAJfClusFfiFneiJAXfilGenfiFneiJA
61 58 60 sstrd FFilXAJfClusFFXfilGenfiFneiJA
62 57 unssbd FFilXAJfClusFneiJAfiFneiJA
63 62 60 sstrd FFilXAJfClusFneiJAXfilGenfiFneiJA
64 elflim JTopOnXXfilGenfiFneiJAFilXAJfLimXfilGenfiFneiJAAXneiJAXfilGenfiFneiJA
65 31 51 64 syl2anc FFilXAJfClusFAJfLimXfilGenfiFneiJAAXneiJAXfilGenfiFneiJA
66 34 63 65 mpbir2and FFilXAJfClusFAJfLimXfilGenfiFneiJA
67 sseq2 g=XfilGenfiFneiJAFgFXfilGenfiFneiJA
68 oveq2 g=XfilGenfiFneiJAJfLimg=JfLimXfilGenfiFneiJA
69 68 eleq2d g=XfilGenfiFneiJAAJfLimgAJfLimXfilGenfiFneiJA
70 67 69 anbi12d g=XfilGenfiFneiJAFgAJfLimgFXfilGenfiFneiJAAJfLimXfilGenfiFneiJA
71 70 rspcev XfilGenfiFneiJAFilXFXfilGenfiFneiJAAJfLimXfilGenfiFneiJAgFilXFgAJfLimg
72 51 61 66 71 syl12anc FFilXAJfClusFgFilXFgAJfLimg
73 72 ex FFilXAJfClusFgFilXFgAJfLimg
74 simprl FFilXgFilXFgAJfLimggFilX
75 simprrr FFilXgFilXFgAJfLimgAJfLimg
76 flimtopon AJfLimgJTopOnXgFilX
77 75 76 syl FFilXgFilXFgAJfLimgJTopOnXgFilX
78 74 77 mpbird FFilXgFilXFgAJfLimgJTopOnX
79 simpl FFilXgFilXFgAJfLimgFFilX
80 simprrl FFilXgFilXFgAJfLimgFg
81 fclsss2 JTopOnXFFilXFgJfClusgJfClusF
82 78 79 80 81 syl3anc FFilXgFilXFgAJfLimgJfClusgJfClusF
83 flimfcls JfLimgJfClusg
84 83 75 sselid FFilXgFilXFgAJfLimgAJfClusg
85 82 84 sseldd FFilXgFilXFgAJfLimgAJfClusF
86 85 rexlimdvaa FFilXgFilXFgAJfLimgAJfClusF
87 73 86 impbid FFilXAJfClusFgFilXFgAJfLimg