# 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 ${⊢}{\phi }\to {F}:{A}⟶ℂ$
limcflf.a ${⊢}{\phi }\to {A}\subseteq ℂ$
limcflf.b ${⊢}{\phi }\to {B}\in \mathrm{limPt}\left({K}\right)\left({A}\right)$
limcflf.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
limcflf.c ${⊢}{C}={A}\setminus \left\{{B}\right\}$
limcflf.l ${⊢}{L}=\mathrm{nei}\left({K}\right)\left(\left\{{B}\right\}\right){↾}_{𝑡}{C}$
Assertion limcflf ${⊢}{\phi }\to {F}{lim}_{ℂ}{B}=\left({K}\mathrm{fLimf}{L}\right)\left({{F}↾}_{{C}}\right)$

### Proof

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