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 φBlimPtKA
limcflf.k K=TopOpenfld
limcflf.c C=AB
limcflf.l L=neiKB𝑡C
Assertion limcflf φFlimB=KfLimfLFC

Proof

Step Hyp Ref Expression
1 limcflf.f φF:A
2 limcflf.a φA
3 limcflf.b φBlimPtKA
4 limcflf.k K=TopOpenfld
5 limcflf.c C=AB
6 limcflf.l L=neiKB𝑡C
7 vex tV
8 7 inex1 tCV
9 8 rgenw tneiKBtCV
10 eqid tneiKBtC=tneiKBtC
11 imaeq2 s=tCFCs=FCtC
12 inss2 tCC
13 resima2 tCCFCtC=FtC
14 12 13 ax-mp FCtC=FtC
15 11 14 eqtrdi s=tCFCs=FtC
16 15 sseq1d s=tCFCsuFtCu
17 10 16 rexrnmptw tneiKBtCVsrantneiKBtCFCsutneiKBFtCu
18 9 17 mp1i φxuKxusrantneiKBtCFCsutneiKBFtCu
19 fvex neiKBV
20 difss ABA
21 5 20 eqsstri CA
22 21 2 sstrid φC
23 cnex V
24 23 ssex CCV
25 22 24 syl φCV
26 25 ad2antrr φxuKxuCV
27 restval neiKBVCVneiKB𝑡C=rantneiKBtC
28 19 26 27 sylancr φxuKxuneiKB𝑡C=rantneiKBtC
29 6 28 eqtrid φxuKxuL=rantneiKBtC
30 29 rexeqdv φxuKxusLFCsusrantneiKBtCFCsu
31 4 cnfldtop KTop
32 opnneip KTopwKBwwneiKB
33 31 32 mp3an1 wKBwwneiKB
34 id t=wt=w
35 5 a1i t=wC=AB
36 34 35 ineq12d t=wtC=wAB
37 36 imaeq2d t=wFtC=FwAB
38 37 sseq1d t=wFtCuFwABu
39 38 rspcev wneiKBFwAButneiKBFtCu
40 33 39 sylan wKBwFwAButneiKBFtCu
41 40 anasss wKBwFwAButneiKBFtCu
42 41 rexlimiva wKBwFwAButneiKBFtCu
43 simprl φxuKxutneiKBFtCutneiKB
44 4 cnfldtopon KTopOn
45 44 toponunii =K
46 45 neii1 KToptneiKBt
47 31 43 46 sylancr φxuKxutneiKBFtCut
48 45 ntropn KToptintKtK
49 31 47 48 sylancr φxuKxutneiKBFtCuintKtK
50 45 lpss KTopAlimPtKA
51 31 2 50 sylancr φlimPtKA
52 51 3 sseldd φB
53 52 snssd φB
54 53 ad3antrrr φxuKxutneiKBFtCuB
55 45 neiint KTopBttneiKBBintKt
56 31 54 47 55 mp3an2i φxuKxutneiKBFtCutneiKBBintKt
57 43 56 mpbid φxuKxutneiKBFtCuBintKt
58 52 ad3antrrr φxuKxutneiKBFtCuB
59 snssg BBintKtBintKt
60 58 59 syl φxuKxutneiKBFtCuBintKtBintKt
61 57 60 mpbird φxuKxutneiKBFtCuBintKt
62 45 ntrss2 KToptintKtt
63 31 47 62 sylancr φxuKxutneiKBFtCuintKtt
64 ssrin intKttintKtCtC
65 imass2 intKtCtCFintKtCFtC
66 63 64 65 3syl φxuKxutneiKBFtCuFintKtCFtC
67 simprr φxuKxutneiKBFtCuFtCu
68 66 67 sstrd φxuKxutneiKBFtCuFintKtCu
69 eleq2 w=intKtBwBintKt
70 5 ineq2i wC=wAB
71 ineq1 w=intKtwC=intKtC
72 70 71 eqtr3id w=intKtwAB=intKtC
73 72 imaeq2d w=intKtFwAB=FintKtC
74 73 sseq1d w=intKtFwABuFintKtCu
75 69 74 anbi12d w=intKtBwFwABuBintKtFintKtCu
76 75 rspcev intKtKBintKtFintKtCuwKBwFwABu
77 49 61 68 76 syl12anc φxuKxutneiKBFtCuwKBwFwABu
78 77 rexlimdvaa φxuKxutneiKBFtCuwKBwFwABu
79 42 78 impbid2 φxuKxuwKBwFwAButneiKBFtCu
80 18 30 79 3bitr4rd φxuKxuwKBwFwABusLFCsu
81 80 anassrs φxuKxuwKBwFwABusLFCsu
82 81 pm5.74da φxuKxuwKBwFwABuxusLFCsu
83 82 ralbidva φxuKxuwKBwFwABuuKxusLFCsu
84 83 pm5.32da φxuKxuwKBwFwABuxuKxusLFCsu
85 1 2 52 4 ellimc2 φxFlimBxuKxuwKBwFwABu
86 1 2 3 4 5 6 limcflflem φLFilC
87 fssres F:ACAFC:C
88 1 21 87 sylancl φFC:C
89 isflf KTopOnLFilCFC:CxKfLimfLFCxuKxusLFCsu
90 44 86 88 89 mp3an2i φxKfLimfLFCxuKxusLFCsu
91 84 85 90 3bitr4d φxFlimBxKfLimfLFC
92 91 eqrdv φFlimB=KfLimfLFC