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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limcresioolb.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
limcresioolb.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
limcresioolb.bltc ⊢ ( 𝜑 → 𝐵 < 𝐶 )
limcresioolb.bcss ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ 𝐴 )
limcresioolb.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
limcresioolb.cled ⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
Assertion limcresioolb ( 𝜑 → ( ( 𝐹 ↾ ( 𝐵 (,) 𝐶 ) ) limℂ 𝐵 ) = ( ( 𝐹 ↾ ( 𝐵 (,) 𝐷 ) ) limℂ 𝐵 ) )

Proof

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