Metamath Proof Explorer

Theorem limcnlp

Description: If B is not a limit point of the domain of the function F , then every point is a limit of F at B . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limccl.f 
|- ( ph -> F : A --> CC )
limccl.a 
|- ( ph -> A C_ CC )
limccl.b 
|- ( ph -> B e. CC )
ellimc2.k 
|- K = ( TopOpen ` CCfld )
limcnlp.n 
|- ( ph -> -. B e. ( ( limPt ` K ) ` A ) )
Assertion limcnlp 
|- ( ph -> ( F limCC B ) = CC )

Proof

Step Hyp Ref Expression
1 limccl.f 
 |-  ( ph -> F : A --> CC )
2 limccl.a 
 |-  ( ph -> A C_ CC )
3 limccl.b 
 |-  ( ph -> B e. CC )
4 ellimc2.k 
 |-  K = ( TopOpen ` CCfld )
5 limcnlp.n 
 |-  ( ph -> -. B e. ( ( limPt ` K ) ` A ) )
6 1 2 3 4 ellimc2 
 |-  ( ph -> ( x e. ( F limCC B ) <-> ( x e. CC /\ A. u e. K ( x e. u -> E. v e. K ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) ) )
7 4 cnfldtop 
 |-  K e. Top
8 2 adantr 
 |-  ( ( ph /\ x e. CC ) -> A C_ CC )
9 8 ssdifssd 
 |-  ( ( ph /\ x e. CC ) -> ( A \ { B } ) C_ CC )
10 4 cnfldtopon 
 |-  K e. ( TopOn ` CC )
11 10 toponunii 
 |-  CC = U. K
12 11 clscld 
 |-  ( ( K e. Top /\ ( A \ { B } ) C_ CC ) -> ( ( cls ` K ) ` ( A \ { B } ) ) e. ( Clsd ` K ) )
13 7 9 12 sylancr 
 |-  ( ( ph /\ x e. CC ) -> ( ( cls ` K ) ` ( A \ { B } ) ) e. ( Clsd ` K ) )
14 11 cldopn 
 |-  ( ( ( cls ` K ) ` ( A \ { B } ) ) e. ( Clsd ` K ) -> ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) e. K )
15 13 14 syl 
 |-  ( ( ph /\ x e. CC ) -> ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) e. K )
16 11 islp 
 |-  ( ( K e. Top /\ A C_ CC ) -> ( B e. ( ( limPt ` K ) ` A ) <-> B e. ( ( cls ` K ) ` ( A \ { B } ) ) ) )
17 7 2 16 sylancr 
 |-  ( ph -> ( B e. ( ( limPt ` K ) ` A ) <-> B e. ( ( cls ` K ) ` ( A \ { B } ) ) ) )
18 5 17 mtbid 
 |-  ( ph -> -. B e. ( ( cls ` K ) ` ( A \ { B } ) ) )
19 3 18 eldifd 
 |-  ( ph -> B e. ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) )
20 19 adantr 
 |-  ( ( ph /\ x e. CC ) -> B e. ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) )
21 difin2 
 |-  ( ( A \ { B } ) C_ CC -> ( ( A \ { B } ) \ ( ( cls ` K ) ` ( A \ { B } ) ) ) = ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) )
22 9 21 syl 
 |-  ( ( ph /\ x e. CC ) -> ( ( A \ { B } ) \ ( ( cls ` K ) ` ( A \ { B } ) ) ) = ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) )
23 11 sscls 
 |-  ( ( K e. Top /\ ( A \ { B } ) C_ CC ) -> ( A \ { B } ) C_ ( ( cls ` K ) ` ( A \ { B } ) ) )
24 7 9 23 sylancr 
 |-  ( ( ph /\ x e. CC ) -> ( A \ { B } ) C_ ( ( cls ` K ) ` ( A \ { B } ) ) )
25 ssdif0 
 |-  ( ( A \ { B } ) C_ ( ( cls ` K ) ` ( A \ { B } ) ) <-> ( ( A \ { B } ) \ ( ( cls ` K ) ` ( A \ { B } ) ) ) = (/) )
26 24 25 sylib 
 |-  ( ( ph /\ x e. CC ) -> ( ( A \ { B } ) \ ( ( cls ` K ) ` ( A \ { B } ) ) ) = (/) )
27 22 26 eqtr3d 
 |-  ( ( ph /\ x e. CC ) -> ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) = (/) )
28 27 imaeq2d 
 |-  ( ( ph /\ x e. CC ) -> ( F " ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) ) = ( F " (/) ) )
29 ima0 
 |-  ( F " (/) ) = (/)
30 28 29 eqtrdi 
 |-  ( ( ph /\ x e. CC ) -> ( F " ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) ) = (/) )
31 0ss 
 |-  (/) C_ u
32 30 31 eqsstrdi 
 |-  ( ( ph /\ x e. CC ) -> ( F " ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) ) C_ u )
33 eleq2 
 |-  ( v = ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) -> ( B e. v <-> B e. ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) ) )
34 ineq1 
 |-  ( v = ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) -> ( v i^i ( A \ { B } ) ) = ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) )
35 34 imaeq2d 
 |-  ( v = ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) -> ( F " ( v i^i ( A \ { B } ) ) ) = ( F " ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) ) )
36 35 sseq1d 
 |-  ( v = ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) -> ( ( F " ( v i^i ( A \ { B } ) ) ) C_ u <-> ( F " ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) ) C_ u ) )
37 33 36 anbi12d 
 |-  ( v = ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) -> ( ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) <-> ( B e. ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) /\ ( F " ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) ) C_ u ) ) )
38 37 rspcev 
 |-  ( ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) e. K /\ ( B e. ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) /\ ( F " ( ( CC \ ( ( cls ` K ) ` ( A \ { B } ) ) ) i^i ( A \ { B } ) ) ) C_ u ) ) -> E. v e. K ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) )
39 15 20 32 38 syl12anc 
 |-  ( ( ph /\ x e. CC ) -> E. v e. K ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) )
40 39 a1d 
 |-  ( ( ph /\ x e. CC ) -> ( x e. u -> E. v e. K ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) )
41 40 ralrimivw 
 |-  ( ( ph /\ x e. CC ) -> A. u e. K ( x e. u -> E. v e. K ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) )
42 41 ex 
 |-  ( ph -> ( x e. CC -> A. u e. K ( x e. u -> E. v e. K ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) )
43 42 pm4.71d 
 |-  ( ph -> ( x e. CC <-> ( x e. CC /\ A. u e. K ( x e. u -> E. v e. K ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) ) )
44 6 43 bitr4d 
 |-  ( ph -> ( x e. ( F limCC B ) <-> x e. CC ) )
45 44 eqrdv 
 |-  ( ph -> ( F limCC B ) = CC )