Metamath Proof Explorer


Theorem limcres

Description: If B is an interior point of C u. { B } relative to the domain A , then a limit point of ` F |`C extends to a limit of F . (Contributed by Mario Carneiro, 27-Dec-2016)

Ref Expression
Hypotheses limcres.f
|- ( ph -> F : A --> CC )
limcres.c
|- ( ph -> C C_ A )
limcres.a
|- ( ph -> A C_ CC )
limcres.k
|- K = ( TopOpen ` CCfld )
limcres.j
|- J = ( K |`t ( A u. { B } ) )
limcres.i
|- ( ph -> B e. ( ( int ` J ) ` ( C u. { B } ) ) )
Assertion limcres
|- ( ph -> ( ( F |` C ) limCC B ) = ( F limCC B ) )

Proof

Step Hyp Ref Expression
1 limcres.f
 |-  ( ph -> F : A --> CC )
2 limcres.c
 |-  ( ph -> C C_ A )
3 limcres.a
 |-  ( ph -> A C_ CC )
4 limcres.k
 |-  K = ( TopOpen ` CCfld )
5 limcres.j
 |-  J = ( K |`t ( A u. { B } ) )
6 limcres.i
 |-  ( ph -> B e. ( ( int ` J ) ` ( C u. { B } ) ) )
7 limcrcl
 |-  ( x e. ( ( F |` C ) limCC B ) -> ( ( F |` C ) : dom ( F |` C ) --> CC /\ dom ( F |` C ) C_ CC /\ B e. CC ) )
8 7 simp3d
 |-  ( x e. ( ( F |` C ) limCC B ) -> B e. CC )
9 limccl
 |-  ( ( F |` C ) limCC B ) C_ CC
10 9 sseli
 |-  ( x e. ( ( F |` C ) limCC B ) -> x e. CC )
11 8 10 jca
 |-  ( x e. ( ( F |` C ) limCC B ) -> ( B e. CC /\ x e. CC ) )
12 11 a1i
 |-  ( ph -> ( x e. ( ( F |` C ) limCC B ) -> ( B e. CC /\ x e. CC ) ) )
13 limcrcl
 |-  ( x e. ( F limCC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
14 13 simp3d
 |-  ( x e. ( F limCC B ) -> B e. CC )
15 limccl
 |-  ( F limCC B ) C_ CC
16 15 sseli
 |-  ( x e. ( F limCC B ) -> x e. CC )
17 14 16 jca
 |-  ( x e. ( F limCC B ) -> ( B e. CC /\ x e. CC ) )
18 17 a1i
 |-  ( ph -> ( x e. ( F limCC B ) -> ( B e. CC /\ x e. CC ) ) )
19 4 cnfldtopon
 |-  K e. ( TopOn ` CC )
20 3 adantr
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> A C_ CC )
21 simprl
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> B e. CC )
22 21 snssd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> { B } C_ CC )
23 20 22 unssd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( A u. { B } ) C_ CC )
24 resttopon
 |-  ( ( K e. ( TopOn ` CC ) /\ ( A u. { B } ) C_ CC ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
25 19 23 24 sylancr
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
26 5 25 eqeltrid
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> J e. ( TopOn ` ( A u. { B } ) ) )
27 topontop
 |-  ( J e. ( TopOn ` ( A u. { B } ) ) -> J e. Top )
28 26 27 syl
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> J e. Top )
29 2 adantr
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> C C_ A )
30 unss1
 |-  ( C C_ A -> ( C u. { B } ) C_ ( A u. { B } ) )
31 29 30 syl
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( C u. { B } ) C_ ( A u. { B } ) )
32 toponuni
 |-  ( J e. ( TopOn ` ( A u. { B } ) ) -> ( A u. { B } ) = U. J )
33 26 32 syl
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( A u. { B } ) = U. J )
34 31 33 sseqtrd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( C u. { B } ) C_ U. J )
35 6 adantr
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> B e. ( ( int ` J ) ` ( C u. { B } ) ) )
36 elun
 |-  ( z e. ( A u. { B } ) <-> ( z e. A \/ z e. { B } ) )
37 simplrr
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ z e. A ) -> x e. CC )
38 1 adantr
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> F : A --> CC )
39 38 ffvelrnda
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ z e. A ) -> ( F ` z ) e. CC )
40 37 39 ifcld
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ z e. A ) -> if ( z = B , x , ( F ` z ) ) e. CC )
41 elsni
 |-  ( z e. { B } -> z = B )
42 41 adantl
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ z e. { B } ) -> z = B )
43 42 iftrued
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ z e. { B } ) -> if ( z = B , x , ( F ` z ) ) = x )
44 simplrr
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ z e. { B } ) -> x e. CC )
45 43 44 eqeltrd
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ z e. { B } ) -> if ( z = B , x , ( F ` z ) ) e. CC )
46 40 45 jaodan
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ ( z e. A \/ z e. { B } ) ) -> if ( z = B , x , ( F ` z ) ) e. CC )
47 36 46 sylan2b
 |-  ( ( ( ph /\ ( B e. CC /\ x e. CC ) ) /\ z e. ( A u. { B } ) ) -> if ( z = B , x , ( F ` z ) ) e. CC )
48 47 fmpttd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) : ( A u. { B } ) --> CC )
49 33 feq2d
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) : ( A u. { B } ) --> CC <-> ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) : U. J --> CC ) )
50 48 49 mpbid
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) : U. J --> CC )
51 eqid
 |-  U. J = U. J
52 19 toponunii
 |-  CC = U. K
53 51 52 cnprest
 |-  ( ( ( J e. Top /\ ( C u. { B } ) C_ U. J ) /\ ( B e. ( ( int ` J ) ` ( C u. { B } ) ) /\ ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) : U. J --> CC ) ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) <-> ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) |` ( C u. { B } ) ) e. ( ( ( J |`t ( C u. { B } ) ) CnP K ) ` B ) ) )
54 28 34 35 50 53 syl22anc
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) <-> ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) |` ( C u. { B } ) ) e. ( ( ( J |`t ( C u. { B } ) ) CnP K ) ` B ) ) )
55 eqid
 |-  ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) = ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) )
56 5 4 55 38 20 21 ellimc
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( x e. ( F limCC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) ) )
57 eqid
 |-  ( K |`t ( C u. { B } ) ) = ( K |`t ( C u. { B } ) )
58 eqid
 |-  ( z e. ( C u. { B } ) |-> if ( z = B , x , ( ( F |` C ) ` z ) ) ) = ( z e. ( C u. { B } ) |-> if ( z = B , x , ( ( F |` C ) ` z ) ) )
59 38 29 fssresd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( F |` C ) : C --> CC )
60 29 20 sstrd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> C C_ CC )
61 57 4 58 59 60 21 ellimc
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( x e. ( ( F |` C ) limCC B ) <-> ( z e. ( C u. { B } ) |-> if ( z = B , x , ( ( F |` C ) ` z ) ) ) e. ( ( ( K |`t ( C u. { B } ) ) CnP K ) ` B ) ) )
62 elun
 |-  ( z e. ( C u. { B } ) <-> ( z e. C \/ z e. { B } ) )
63 velsn
 |-  ( z e. { B } <-> z = B )
64 63 orbi2i
 |-  ( ( z e. C \/ z e. { B } ) <-> ( z e. C \/ z = B ) )
65 62 64 bitri
 |-  ( z e. ( C u. { B } ) <-> ( z e. C \/ z = B ) )
66 pm5.61
 |-  ( ( ( z e. C \/ z = B ) /\ -. z = B ) <-> ( z e. C /\ -. z = B ) )
67 fvres
 |-  ( z e. C -> ( ( F |` C ) ` z ) = ( F ` z ) )
68 67 adantr
 |-  ( ( z e. C /\ -. z = B ) -> ( ( F |` C ) ` z ) = ( F ` z ) )
69 66 68 sylbi
 |-  ( ( ( z e. C \/ z = B ) /\ -. z = B ) -> ( ( F |` C ) ` z ) = ( F ` z ) )
70 69 ifeq2da
 |-  ( ( z e. C \/ z = B ) -> if ( z = B , x , ( ( F |` C ) ` z ) ) = if ( z = B , x , ( F ` z ) ) )
71 65 70 sylbi
 |-  ( z e. ( C u. { B } ) -> if ( z = B , x , ( ( F |` C ) ` z ) ) = if ( z = B , x , ( F ` z ) ) )
72 71 mpteq2ia
 |-  ( z e. ( C u. { B } ) |-> if ( z = B , x , ( ( F |` C ) ` z ) ) ) = ( z e. ( C u. { B } ) |-> if ( z = B , x , ( F ` z ) ) )
73 31 resmptd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) |` ( C u. { B } ) ) = ( z e. ( C u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) )
74 72 73 eqtr4id
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( z e. ( C u. { B } ) |-> if ( z = B , x , ( ( F |` C ) ` z ) ) ) = ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) |` ( C u. { B } ) ) )
75 5 oveq1i
 |-  ( J |`t ( C u. { B } ) ) = ( ( K |`t ( A u. { B } ) ) |`t ( C u. { B } ) )
76 cnex
 |-  CC e. _V
77 76 ssex
 |-  ( ( A u. { B } ) C_ CC -> ( A u. { B } ) e. _V )
78 23 77 syl
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( A u. { B } ) e. _V )
79 restabs
 |-  ( ( K e. ( TopOn ` CC ) /\ ( C u. { B } ) C_ ( A u. { B } ) /\ ( A u. { B } ) e. _V ) -> ( ( K |`t ( A u. { B } ) ) |`t ( C u. { B } ) ) = ( K |`t ( C u. { B } ) ) )
80 19 31 78 79 mp3an2i
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( ( K |`t ( A u. { B } ) ) |`t ( C u. { B } ) ) = ( K |`t ( C u. { B } ) ) )
81 75 80 eqtr2id
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( K |`t ( C u. { B } ) ) = ( J |`t ( C u. { B } ) ) )
82 81 oveq1d
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( ( K |`t ( C u. { B } ) ) CnP K ) = ( ( J |`t ( C u. { B } ) ) CnP K ) )
83 82 fveq1d
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( ( ( K |`t ( C u. { B } ) ) CnP K ) ` B ) = ( ( ( J |`t ( C u. { B } ) ) CnP K ) ` B ) )
84 74 83 eleq12d
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( ( z e. ( C u. { B } ) |-> if ( z = B , x , ( ( F |` C ) ` z ) ) ) e. ( ( ( K |`t ( C u. { B } ) ) CnP K ) ` B ) <-> ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) |` ( C u. { B } ) ) e. ( ( ( J |`t ( C u. { B } ) ) CnP K ) ` B ) ) )
85 61 84 bitrd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( x e. ( ( F |` C ) limCC B ) <-> ( ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) |` ( C u. { B } ) ) e. ( ( ( J |`t ( C u. { B } ) ) CnP K ) ` B ) ) )
86 54 56 85 3bitr4rd
 |-  ( ( ph /\ ( B e. CC /\ x e. CC ) ) -> ( x e. ( ( F |` C ) limCC B ) <-> x e. ( F limCC B ) ) )
87 86 ex
 |-  ( ph -> ( ( B e. CC /\ x e. CC ) -> ( x e. ( ( F |` C ) limCC B ) <-> x e. ( F limCC B ) ) ) )
88 12 18 87 pm5.21ndd
 |-  ( ph -> ( x e. ( ( F |` C ) limCC B ) <-> x e. ( F limCC B ) ) )
89 88 eqrdv
 |-  ( ph -> ( ( F |` C ) limCC B ) = ( F limCC B ) )