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 F Fil X A J fClus F g Fil X F g A J fLim g

Proof

Step Hyp Ref Expression
1 filsspw F Fil X F 𝒫 X
2 1 adantr F Fil X A J fClus F F 𝒫 X
3 fclstop A J fClus F J Top
4 3 adantl F Fil X A J fClus F J Top
5 eqid J = J
6 5 neisspw J Top nei J A 𝒫 J
7 4 6 syl F Fil X A J fClus F nei J A 𝒫 J
8 filunibas F Fil X F = X
9 5 fclsfil A J fClus F F Fil J
10 filunibas F Fil J F = J
11 9 10 syl A J fClus F F = J
12 8 11 sylan9req F Fil X A J fClus F X = J
13 12 pweqd F Fil X A J fClus F 𝒫 X = 𝒫 J
14 7 13 sseqtrrd F Fil X A J fClus F nei J A 𝒫 X
15 2 14 unssd F Fil X A J fClus F F nei J A 𝒫 X
16 ssun1 F F nei J A
17 filn0 F Fil X F
18 ssn0 F F nei J A F F nei J A
19 16 17 18 sylancr F Fil X F nei J A
20 19 adantr F Fil X A J fClus F F nei J A
21 incom y x = x y
22 fclsneii A J fClus F y nei J A x F y x
23 21 22 eqnetrrid A J fClus F y nei J A x F x y
24 23 3com23 A J fClus F x F y nei J A x y
25 24 3expb A J fClus F x F y nei J A x y
26 25 adantll F Fil X A J fClus F x F y nei J A x y
27 26 ralrimivva F Fil X A J fClus F x F y nei J A x y
28 filfbas F Fil X F fBas X
29 28 adantr F Fil X A J fClus F F fBas X
30 istopon J TopOn X J Top X = J
31 4 12 30 sylanbrc F Fil X A J fClus F J TopOn X
32 5 fclselbas A J fClus F A J
33 32 adantl F Fil X A J fClus F A J
34 33 12 eleqtrrd F Fil X A J fClus F A X
35 34 snssd F Fil X A J fClus F A X
36 snnzg A J fClus F A
37 36 adantl F Fil X A J fClus F A
38 neifil J TopOn X A X A nei J A Fil X
39 31 35 37 38 syl3anc F Fil X A J fClus F nei J A Fil X
40 filfbas nei J A Fil X nei J A fBas X
41 39 40 syl F Fil X A J fClus F nei J A fBas X
42 fbunfip F fBas X nei J A fBas X ¬ fi F nei J A x F y nei J A x y
43 29 41 42 syl2anc F Fil X A J fClus F ¬ fi F nei J A x F y nei J A x y
44 27 43 mpbird F Fil X A J fClus F ¬ fi F nei J A
45 filtop F Fil X X F
46 fsubbas X F fi F nei J A fBas X F nei J A 𝒫 X F nei J A ¬ fi F nei J A
47 45 46 syl F Fil X fi F nei J A fBas X F nei J A 𝒫 X F nei J A ¬ fi F nei J A
48 47 adantr F Fil X A J fClus F fi F nei J A fBas X F nei J A 𝒫 X F nei J A ¬ fi F nei J A
49 15 20 44 48 mpbir3and F Fil X A J fClus F fi F nei J A fBas X
50 fgcl fi F nei J A fBas X X filGen fi F nei J A Fil X
51 49 50 syl F Fil X A J fClus F X filGen fi F nei J A Fil X
52 fvex nei J A V
53 unexg F Fil X nei J A V F nei J A V
54 52 53 mpan2 F Fil X F nei J A V
55 ssfii F nei J A V F nei J A fi F nei J A
56 54 55 syl F Fil X F nei J A fi F nei J A
57 56 adantr F Fil X A J fClus F F nei J A fi F nei J A
58 57 unssad F Fil X A J fClus F F fi F nei J A
59 ssfg fi F nei J A fBas X fi F nei J A X filGen fi F nei J A
60 49 59 syl F Fil X A J fClus F fi F nei J A X filGen fi F nei J A
61 58 60 sstrd F Fil X A J fClus F F X filGen fi F nei J A
62 57 unssbd F Fil X A J fClus F nei J A fi F nei J A
63 62 60 sstrd F Fil X A J fClus F nei J A X filGen fi F nei J A
64 elflim J TopOn X X filGen fi F nei J A Fil X A J fLim X filGen fi F nei J A A X nei J A X filGen fi F nei J A
65 31 51 64 syl2anc F Fil X A J fClus F A J fLim X filGen fi F nei J A A X nei J A X filGen fi F nei J A
66 34 63 65 mpbir2and F Fil X A J fClus F A J fLim X filGen fi F nei J A
67 sseq2 g = X filGen fi F nei J A F g F X filGen fi F nei J A
68 oveq2 g = X filGen fi F nei J A J fLim g = J fLim X filGen fi F nei J A
69 68 eleq2d g = X filGen fi F nei J A A J fLim g A J fLim X filGen fi F nei J A
70 67 69 anbi12d g = X filGen fi F nei J A F g A J fLim g F X filGen fi F nei J A A J fLim X filGen fi F nei J A
71 70 rspcev X filGen fi F nei J A Fil X F X filGen fi F nei J A A J fLim X filGen fi F nei J A g Fil X F g A J fLim g
72 51 61 66 71 syl12anc F Fil X A J fClus F g Fil X F g A J fLim g
73 72 ex F Fil X A J fClus F g Fil X F g A J fLim g
74 simprl F Fil X g Fil X F g A J fLim g g Fil X
75 simprrr F Fil X g Fil X F g A J fLim g A J fLim g
76 flimtopon A J fLim g J TopOn X g Fil X
77 75 76 syl F Fil X g Fil X F g A J fLim g J TopOn X g Fil X
78 74 77 mpbird F Fil X g Fil X F g A J fLim g J TopOn X
79 simpl F Fil X g Fil X F g A J fLim g F Fil X
80 simprrl F Fil X g Fil X F g A J fLim g F g
81 fclsss2 J TopOn X F Fil X F g J fClus g J fClus F
82 78 79 80 81 syl3anc F Fil X g Fil X F g A J fLim g J fClus g J fClus F
83 flimfcls J fLim g J fClus g
84 83 75 sselid F Fil X g Fil X F g A J fLim g A J fClus g
85 82 84 sseldd F Fil X g Fil X F g A J fLim g A J fClus F
86 85 rexlimdvaa F Fil X g Fil X F g A J fLim g A J fClus F
87 73 86 impbid F Fil X A J fClus F g Fil X F g A J fLim g