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 
|- ( ph -> F : A --> CC )
limcflf.a 
|- ( ph -> A C_ CC )
limcflf.b 
|- ( ph -> B e. ( ( limPt ` K ) ` A ) )
limcflf.k 
|- K = ( TopOpen ` CCfld )
limcflf.c 
|- C = ( A \ { B } )
limcflf.l 
|- L = ( ( ( nei ` K ) ` { B } ) |`t C )
Assertion limcflf 
|- ( ph -> ( F limCC B ) = ( ( K fLimf L ) ` ( F |` C ) ) )

Proof

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