Metamath Proof Explorer


Theorem limcflf

Description: The limit operator can be expressed as a filter limit, from the filter of neighborhoods of B restricted to A \ { B } , to the topology of the complex numbers. (If B is not a limit point of A , then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcflf.f φ F : A
limcflf.a φ A
limcflf.b φ B limPt K A
limcflf.k K = TopOpen fld
limcflf.c C = A B
limcflf.l L = nei K B 𝑡 C
Assertion limcflf φ F lim B = K fLimf L F C

Proof

Step Hyp Ref Expression
1 limcflf.f φ F : A
2 limcflf.a φ A
3 limcflf.b φ B limPt K A
4 limcflf.k K = TopOpen fld
5 limcflf.c C = A B
6 limcflf.l L = nei K B 𝑡 C
7 vex t V
8 7 inex1 t C V
9 8 rgenw t nei K B t C V
10 eqid t nei K B t C = t nei K B t C
11 imaeq2 s = t C F C s = F C t C
12 inss2 t C C
13 resima2 t C C F C t C = F t C
14 12 13 ax-mp F C t C = F t C
15 11 14 syl6eq s = t C F C s = F t C
16 15 sseq1d s = t C F C s u F t C u
17 10 16 rexrnmptw t nei K B t C V s ran t nei K B t C F C s u t nei K B F t C u
18 9 17 mp1i φ x u K x u s ran t nei K B t C F C s u t nei K B F t C u
19 fvex nei K B V
20 difss A B A
21 5 20 eqsstri C A
22 21 2 sstrid φ C
23 cnex V
24 23 ssex C C V
25 22 24 syl φ C V
26 25 ad2antrr φ x u K x u C V
27 restval nei K B V C V nei K B 𝑡 C = ran t nei K B t C
28 19 26 27 sylancr φ x u K x u nei K B 𝑡 C = ran t nei K B t C
29 6 28 syl5eq φ x u K x u L = ran t nei K B t C
30 29 rexeqdv φ x u K x u s L F C s u s ran t nei K B t C F C s u
31 4 cnfldtop K Top
32 opnneip K Top w K B w w nei K B
33 31 32 mp3an1 w K B w w nei K B
34 id t = w t = w
35 5 a1i t = w C = A B
36 34 35 ineq12d t = w t C = w A B
37 36 imaeq2d t = w F t C = F w A B
38 37 sseq1d t = w F t C u F w A B u
39 38 rspcev w nei K B F w A B u t nei K B F t C u
40 33 39 sylan w K B w F w A B u t nei K B F t C u
41 40 anasss w K B w F w A B u t nei K B F t C u
42 41 rexlimiva w K B w F w A B u t nei K B F t C u
43 simprl φ x u K x u t nei K B F t C u t nei K B
44 4 cnfldtopon K TopOn
45 44 toponunii = K
46 45 neii1 K Top t nei K B t
47 31 43 46 sylancr φ x u K x u t nei K B F t C u t
48 45 ntropn K Top t int K t K
49 31 47 48 sylancr φ x u K x u t nei K B F t C u int K t K
50 45 lpss K Top A limPt K A
51 31 2 50 sylancr φ limPt K A
52 51 3 sseldd φ B
53 52 snssd φ B
54 53 ad3antrrr φ x u K x u t nei K B F t C u B
55 45 neiint K Top B t t nei K B B int K t
56 31 54 47 55 mp3an2i φ x u K x u t nei K B F t C u t nei K B B int K t
57 43 56 mpbid φ x u K x u t nei K B F t C u B int K t
58 52 ad3antrrr φ x u K x u t nei K B F t C u B
59 snssg B B int K t B int K t
60 58 59 syl φ x u K x u t nei K B F t C u B int K t B int K t
61 57 60 mpbird φ x u K x u t nei K B F t C u B int K t
62 45 ntrss2 K Top t int K t t
63 31 47 62 sylancr φ x u K x u t nei K B F t C u int K t t
64 ssrin int K t t int K t C t C
65 imass2 int K t C t C F int K t C F t C
66 63 64 65 3syl φ x u K x u t nei K B F t C u F int K t C F t C
67 simprr φ x u K x u t nei K B F t C u F t C u
68 66 67 sstrd φ x u K x u t nei K B F t C u F int K t C u
69 eleq2 w = int K t B w B int K t
70 5 ineq2i w C = w A B
71 ineq1 w = int K t w C = int K t C
72 70 71 syl5eqr w = int K t w A B = int K t C
73 72 imaeq2d w = int K t F w A B = F int K t C
74 73 sseq1d w = int K t F w A B u F int K t C u
75 69 74 anbi12d w = int K t B w F w A B u B int K t F int K t C u
76 75 rspcev int K t K B int K t F int K t C u w K B w F w A B u
77 49 61 68 76 syl12anc φ x u K x u t nei K B F t C u w K B w F w A B u
78 77 rexlimdvaa φ x u K x u t nei K B F t C u w K B w F w A B u
79 42 78 impbid2 φ x u K x u w K B w F w A B u t nei K B F t C u
80 18 30 79 3bitr4rd φ x u K x u w K B w F w A B u s L F C s u
81 80 anassrs φ x u K x u w K B w F w A B u s L F C s u
82 81 pm5.74da φ x u K x u w K B w F w A B u x u s L F C s u
83 82 ralbidva φ x u K x u w K B w F w A B u u K x u s L F C s u
84 83 pm5.32da φ x u K x u w K B w F w A B u x u K x u s L F C s u
85 1 2 52 4 ellimc2 φ x F lim B x u K x u w K B w F w A B u
86 1 2 3 4 5 6 limcflflem φ L Fil C
87 fssres F : A C A F C : C
88 1 21 87 sylancl φ F C : C
89 isflf K TopOn L Fil C F C : C x K fLimf L F C x u K x u s L F C s u
90 44 86 88 89 mp3an2i φ x K fLimf L F C x u K x u s L F C s u
91 84 85 90 3bitr4d φ x F lim B x K fLimf L F C
92 91 eqrdv φ F lim B = K fLimf L F C