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 syl5req 
 |-  ( ( 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 ) )