Metamath Proof Explorer

Theorem limcresiooub

Description: The left limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcresiooub.f 
|- ( ph -> F : A --> CC )
limcresiooub.b 
|- ( ph -> B e. RR* )
limcresiooub.c 
|- ( ph -> C e. RR )
limcresiooub.bltc 
|- ( ph -> B < C )
limcresiooub.bcss 
|- ( ph -> ( B (,) C ) C_ A )
limcresiooub.d 
|- ( ph -> D e. RR* )
limcresiooub.cled 
|- ( ph -> D <_ B )
Assertion limcresiooub 
|- ( ph -> ( ( F |` ( B (,) C ) ) limCC C ) = ( ( F |` ( D (,) C ) ) limCC C ) )

Proof

Step Hyp Ref Expression
1 limcresiooub.f 
 |-  ( ph -> F : A --> CC )
2 limcresiooub.b 
 |-  ( ph -> B e. RR* )
3 limcresiooub.c 
 |-  ( ph -> C e. RR )
4 limcresiooub.bltc 
 |-  ( ph -> B < C )
5 limcresiooub.bcss 
 |-  ( ph -> ( B (,) C ) C_ A )
6 limcresiooub.d 
 |-  ( ph -> D e. RR* )
7 limcresiooub.cled 
 |-  ( ph -> D <_ B )
8 iooss1 
 |-  ( ( D e. RR* /\ D <_ B ) -> ( B (,) C ) C_ ( D (,) C ) )
9 6 7 8 syl2anc 
 |-  ( ph -> ( B (,) C ) C_ ( D (,) C ) )
10 9 resabs1d 
 |-  ( ph -> ( ( F |` ( D (,) C ) ) |` ( B (,) C ) ) = ( F |` ( B (,) C ) ) )
11 10 eqcomd 
 |-  ( ph -> ( F |` ( B (,) C ) ) = ( ( F |` ( D (,) C ) ) |` ( B (,) C ) ) )
12 11 oveq1d 
 |-  ( ph -> ( ( F |` ( B (,) C ) ) limCC C ) = ( ( ( F |` ( D (,) C ) ) |` ( B (,) C ) ) limCC C ) )
13 fresin 
 |-  ( F : A --> CC -> ( F |` ( D (,) C ) ) : ( A i^i ( D (,) C ) ) --> CC )
14 1 13 syl 
 |-  ( ph -> ( F |` ( D (,) C ) ) : ( A i^i ( D (,) C ) ) --> CC )
15 5 9 ssind 
 |-  ( ph -> ( B (,) C ) C_ ( A i^i ( D (,) C ) ) )
16 inss2 
 |-  ( A i^i ( D (,) C ) ) C_ ( D (,) C )
17 ioosscn 
 |-  ( D (,) C ) C_ CC
18 16 17 sstri 
 |-  ( A i^i ( D (,) C ) ) C_ CC
19 18 a1i 
 |-  ( ph -> ( A i^i ( D (,) C ) ) C_ CC )
20 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
21 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) )
22 3 rexrd 
 |-  ( ph -> C e. RR* )
23 ubioc1 
 |-  ( ( B e. RR* /\ C e. RR* /\ B < C ) -> C e. ( B (,] C ) )
24 2 22 4 23 syl3anc 
 |-  ( ph -> C e. ( B (,] C ) )
25 ioounsn 
 |-  ( ( B e. RR* /\ C e. RR* /\ B < C ) -> ( ( B (,) C ) u. { C } ) = ( B (,] C ) )
26 2 22 4 25 syl3anc 
 |-  ( ph -> ( ( B (,) C ) u. { C } ) = ( B (,] C ) )
27 26 fveq2d 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) ` ( ( B (,) C ) u. { C } ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) ` ( B (,] C ) ) )
28 20 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
29 ovex 
 |-  ( D (,) C ) e. _V
30 29 inex2 
 |-  ( A i^i ( D (,) C ) ) e. _V
31 snex 
 |-  { C } e. _V
32 30 31 unex 
 |-  ( ( A i^i ( D (,) C ) ) u. { C } ) e. _V
33 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( A i^i ( D (,) C ) ) u. { C } ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) e. Top )
34 28 32 33 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) e. Top
35 34 a1i 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) e. Top )
36 pnfxr 
 |-  +oo e. RR*
37 36 a1i 
 |-  ( ph -> +oo e. RR* )
38 2 xrleidd 
 |-  ( ph -> B <_ B )
39 3 ltpnfd 
 |-  ( ph -> C < +oo )
40 iocssioo 
 |-  ( ( ( B e. RR* /\ +oo e. RR* ) /\ ( B <_ B /\ C < +oo ) ) -> ( B (,] C ) C_ ( B (,) +oo ) )
41 2 37 38 39 40 syl22anc 
 |-  ( ph -> ( B (,] C ) C_ ( B (,) +oo ) )
42 simpr 
 |-  ( ( ph /\ x = C ) -> x = C )
43 snidg 
 |-  ( C e. RR -> C e. { C } )
44 elun2 
 |-  ( C e. { C } -> C e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
45 3 43 44 3syl 
 |-  ( ph -> C e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
46 45 adantr 
 |-  ( ( ph /\ x = C ) -> C e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
47 42 46 eqeltrd 
 |-  ( ( ph /\ x = C ) -> x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
48 47 adantlr 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ x = C ) -> x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
49 simpll 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> ph )
50 2 adantr 
 |-  ( ( ph /\ x e. ( B (,] C ) ) -> B e. RR* )
51 50 adantr 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> B e. RR* )
52 22 adantr 
 |-  ( ( ph /\ x e. ( B (,] C ) ) -> C e. RR* )
53 52 adantr 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> C e. RR* )
54 iocssre 
 |-  ( ( B e. RR* /\ C e. RR ) -> ( B (,] C ) C_ RR )
55 2 3 54 syl2anc 
 |-  ( ph -> ( B (,] C ) C_ RR )
56 55 sselda 
 |-  ( ( ph /\ x e. ( B (,] C ) ) -> x e. RR )
57 56 adantr 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> x e. RR )
58 simpr 
 |-  ( ( ph /\ x e. ( B (,] C ) ) -> x e. ( B (,] C ) )
59 iocgtlb 
 |-  ( ( B e. RR* /\ C e. RR* /\ x e. ( B (,] C ) ) -> B < x )
60 50 52 58 59 syl3anc 
 |-  ( ( ph /\ x e. ( B (,] C ) ) -> B < x )
61 60 adantr 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> B < x )
62 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> C e. RR )
63 iocleub 
 |-  ( ( B e. RR* /\ C e. RR* /\ x e. ( B (,] C ) ) -> x <_ C )
64 50 52 58 63 syl3anc 
 |-  ( ( ph /\ x e. ( B (,] C ) ) -> x <_ C )
65 64 adantr 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> x <_ C )
66 neqne 
 |-  ( -. x = C -> x =/= C )
67 66 adantl 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> x =/= C )
68 67 necomd 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> C =/= x )
69 57 62 65 68 leneltd 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> x < C )
70 51 53 57 61 69 eliood 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> x e. ( B (,) C ) )
71 15 sselda 
 |-  ( ( ph /\ x e. ( B (,) C ) ) -> x e. ( A i^i ( D (,) C ) ) )
72 elun1 
 |-  ( x e. ( A i^i ( D (,) C ) ) -> x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
73 71 72 syl 
 |-  ( ( ph /\ x e. ( B (,) C ) ) -> x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
74 49 70 73 syl2anc 
 |-  ( ( ( ph /\ x e. ( B (,] C ) ) /\ -. x = C ) -> x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
75 48 74 pm2.61dan 
 |-  ( ( ph /\ x e. ( B (,] C ) ) -> x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
76 75 ralrimiva 
 |-  ( ph -> A. x e. ( B (,] C ) x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
77 dfss3 
 |-  ( ( B (,] C ) C_ ( ( A i^i ( D (,) C ) ) u. { C } ) <-> A. x e. ( B (,] C ) x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
78 76 77 sylibr 
 |-  ( ph -> ( B (,] C ) C_ ( ( A i^i ( D (,) C ) ) u. { C } ) )
79 41 78 ssind 
 |-  ( ph -> ( B (,] C ) C_ ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
80 79 sseld 
 |-  ( ph -> ( x e. ( B (,] C ) -> x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) )
81 24 adantr 
 |-  ( ( ph /\ x = C ) -> C e. ( B (,] C ) )
82 42 81 eqeltrd 
 |-  ( ( ph /\ x = C ) -> x e. ( B (,] C ) )
83 82 adantlr 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ x = C ) -> x e. ( B (,] C ) )
84 ioossioc 
 |-  ( B (,) C ) C_ ( B (,] C )
85 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> B e. RR* )
86 22 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> C e. RR* )
87 elinel1 
 |-  ( x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) -> x e. ( B (,) +oo ) )
88 87 elioored 
 |-  ( x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) -> x e. RR )
89 88 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> x e. RR )
90 36 a1i 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> +oo e. RR* )
91 87 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> x e. ( B (,) +oo ) )
92 ioogtlb 
 |-  ( ( B e. RR* /\ +oo e. RR* /\ x e. ( B (,) +oo ) ) -> B < x )
93 85 90 91 92 syl3anc 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> B < x )
94 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> D e. RR* )
95 elinel2 
 |-  ( x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) -> x e. ( ( A i^i ( D (,) C ) ) u. { C } ) )
96 id 
 |-  ( -. x = C -> -. x = C )
97 velsn 
 |-  ( x e. { C } <-> x = C )
98 96 97 sylnibr 
 |-  ( -. x = C -> -. x e. { C } )
99 elunnel2 
 |-  ( ( x e. ( ( A i^i ( D (,) C ) ) u. { C } ) /\ -. x e. { C } ) -> x e. ( A i^i ( D (,) C ) ) )
100 95 98 99 syl2an 
 |-  ( ( x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) /\ -. x = C ) -> x e. ( A i^i ( D (,) C ) ) )
101 16 100 sseldi 
 |-  ( ( x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) /\ -. x = C ) -> x e. ( D (,) C ) )
102 101 adantll 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> x e. ( D (,) C ) )
103 iooltub 
 |-  ( ( D e. RR* /\ C e. RR* /\ x e. ( D (,) C ) ) -> x < C )
104 94 86 102 103 syl3anc 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> x < C )
105 85 86 89 93 104 eliood 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> x e. ( B (,) C ) )
106 84 105 sseldi 
 |-  ( ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) /\ -. x = C ) -> x e. ( B (,] C ) )
107 83 106 pm2.61dan 
 |-  ( ( ph /\ x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) -> x e. ( B (,] C ) )
108 107 ex 
 |-  ( ph -> ( x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) -> x e. ( B (,] C ) ) )
109 80 108 impbid 
 |-  ( ph -> ( x e. ( B (,] C ) <-> x e. ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) )
110 109 eqrdv 
 |-  ( ph -> ( B (,] C ) = ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
111 retop 
 |-  ( topGen ` ran (,) ) e. Top
112 111 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. Top )
113 32 a1i 
 |-  ( ph -> ( ( A i^i ( D (,) C ) ) u. { C } ) e. _V )
114 iooretop 
 |-  ( B (,) +oo ) e. ( topGen ` ran (,) )
115 114 a1i 
 |-  ( ph -> ( B (,) +oo ) e. ( topGen ` ran (,) ) )
116 elrestr 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A i^i ( D (,) C ) ) u. { C } ) e. _V /\ ( B (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
117 112 113 115 116 syl3anc 
 |-  ( ph -> ( ( B (,) +oo ) i^i ( ( A i^i ( D (,) C ) ) u. { C } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
118 110 117 eqeltrd 
 |-  ( ph -> ( B (,] C ) e. ( ( topGen ` ran (,) ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
119 20 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
120 119 oveq1i 
 |-  ( ( topGen ` ran (,) ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) )
121 28 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
122 ioossre 
 |-  ( D (,) C ) C_ RR
123 16 122 sstri 
 |-  ( A i^i ( D (,) C ) ) C_ RR
124 123 a1i 
 |-  ( ph -> ( A i^i ( D (,) C ) ) C_ RR )
125 3 snssd 
 |-  ( ph -> { C } C_ RR )
126 124 125 unssd 
 |-  ( ph -> ( ( A i^i ( D (,) C ) ) u. { C } ) C_ RR )
127 reex 
 |-  RR e. _V
128 127 a1i 
 |-  ( ph -> RR e. _V )
129 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( A i^i ( D (,) C ) ) u. { C } ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
130 121 126 128 129 syl3anc 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
131 120 130 syl5eq 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
132 118 131 eleqtrd 
 |-  ( ph -> ( B (,] C ) e. ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) )
133 isopn3i 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) e. Top /\ ( B (,] C ) e. ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) ` ( B (,] C ) ) = ( B (,] C ) )
134 35 132 133 syl2anc 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) ` ( B (,] C ) ) = ( B (,] C ) )
135 27 134 eqtr2d 
 |-  ( ph -> ( B (,] C ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) ` ( ( B (,) C ) u. { C } ) ) )
136 24 135 eleqtrd 
 |-  ( ph -> C e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A i^i ( D (,) C ) ) u. { C } ) ) ) ` ( ( B (,) C ) u. { C } ) ) )
137 14 15 19 20 21 136 limcres 
 |-  ( ph -> ( ( ( F |` ( D (,) C ) ) |` ( B (,) C ) ) limCC C ) = ( ( F |` ( D (,) C ) ) limCC C ) )
138 12 137 eqtrd 
 |-  ( ph -> ( ( F |` ( B (,) C ) ) limCC C ) = ( ( F |` ( D (,) C ) ) limCC C ) )