Metamath Proof Explorer

Theorem limcresioolb

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

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

Proof

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