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

Proof

Step Hyp Ref Expression
1 limcresiooub.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 limcresiooub.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 limcresiooub.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 limcresiooub.bltc ⊢ ( 𝜑 → 𝐵 < 𝐶 )
5 limcresiooub.bcss ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ 𝐴 )
6 limcresiooub.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
7 limcresiooub.cled ⊢ ( 𝜑 → 𝐷 ≤ 𝐵 )
8 iooss1 ⊢ ( ( 𝐷 ∈ ℝ* ∧ 𝐷 ≤ 𝐵 ) → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝐷 (,) 𝐶 ) )
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 3 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
23 ubioc1 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → 𝐶 ∈ ( 𝐵 (,] 𝐶 ) )
24 2 22 4 23 syl3anc ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 (,] 𝐶 ) )
25 ioounsn ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → ( ( 𝐵 (,) 𝐶 ) ∪ { 𝐶 } ) = ( 𝐵 (,] 𝐶 ) )
26 2 22 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 pnfxr ⊢ +∞ ∈ ℝ*
37 36 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
38 2 xrleidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
39 3 ltpnfd ⊢ ( 𝜑 → 𝐶 < +∞ )
40 iocssioo ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐵 ≤ 𝐵 ∧ 𝐶 < +∞ ) ) → ( 𝐵 (,] 𝐶 ) ⊆ ( 𝐵 (,) +∞ ) )
41 2 37 38 39 40 syl22anc ⊢ ( 𝜑 → ( 𝐵 (,] 𝐶 ) ⊆ ( 𝐵 (,) +∞ ) )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 = 𝐶 )
43 snidg ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ { 𝐶 } )
44 elun2 ⊢ ( 𝐶 ∈ { 𝐶 } → 𝐶 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
45 3 43 44 3syl ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐶 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
47 42 46 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
48 47 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ 𝑥 = 𝐶 ) → 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
49 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝜑 )
50 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐵 ∈ ℝ* )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐵 ∈ ℝ* )
52 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐶 ∈ ℝ* )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐶 ∈ ℝ* )
54 iocssre ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ ) → ( 𝐵 (,] 𝐶 ) ⊆ ℝ )
55 2 3 54 syl2anc ⊢ ( 𝜑 → ( 𝐵 (,] 𝐶 ) ⊆ ℝ )
56 55 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ∈ ℝ )
57 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ℝ )
58 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
59 iocgtlb ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐵 < 𝑥 )
60 50 52 58 59 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝐵 < 𝑥 )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐵 < 𝑥 )
62 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐶 ∈ ℝ )
63 iocleub ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ≤ 𝐶 )
64 50 52 58 63 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ≤ 𝐶 )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ≤ 𝐶 )
66 neqne ⊢ ( ¬ 𝑥 = 𝐶 → 𝑥 ≠ 𝐶 )
67 66 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ≠ 𝐶 )
68 67 necomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐶 ≠ 𝑥 )
69 57 62 65 68 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 < 𝐶 )
70 51 53 57 61 69 eliood ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐵 (,) 𝐶 ) )
71 15 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) )
72 elun1 ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) → 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
73 71 72 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
74 49 70 73 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
75 48 74 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) → 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
76 75 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
77 dfss3 ⊢ ( ( 𝐵 (,] 𝐶 ) ⊆ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ↔ ∀ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
78 76 77 sylibr ⊢ ( 𝜑 → ( 𝐵 (,] 𝐶 ) ⊆ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
79 41 78 ssind ⊢ ( 𝜑 → ( 𝐵 (,] 𝐶 ) ⊆ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
80 79 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 (,] 𝐶 ) → 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) )
81 24 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐶 ∈ ( 𝐵 (,] 𝐶 ) )
82 42 81 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
83 82 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
84 ioossioc ⊢ ( 𝐵 (,) 𝐶 ) ⊆ ( 𝐵 (,] 𝐶 )
85 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐵 ∈ ℝ* )
86 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐶 ∈ ℝ* )
87 elinel1 ⊢ ( 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) → 𝑥 ∈ ( 𝐵 (,) +∞ ) )
88 87 elioored ⊢ ( 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) → 𝑥 ∈ ℝ )
89 88 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ℝ )
90 36 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → +∞ ∈ ℝ* )
91 87 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐵 (,) +∞ ) )
92 ioogtlb ⊢ ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ ( 𝐵 (,) +∞ ) ) → 𝐵 < 𝑥 )
93 85 90 91 92 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐵 < 𝑥 )
94 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝐷 ∈ ℝ* )
95 elinel2 ⊢ ( 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) → 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
96 id ⊢ ( ¬ 𝑥 = 𝐶 → ¬ 𝑥 = 𝐶 )
97 velsn ⊢ ( 𝑥 ∈ { 𝐶 } ↔ 𝑥 = 𝐶 )
98 96 97 sylnibr ⊢ ( ¬ 𝑥 = 𝐶 → ¬ 𝑥 ∈ { 𝐶 } )
99 elunnel2 ⊢ ( ( 𝑥 ∈ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ∧ ¬ 𝑥 ∈ { 𝐶 } ) → 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) )
100 95 98 99 syl2an ⊢ ( ( 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) )
101 16 100 sselid ⊢ ( ( 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐷 (,) 𝐶 ) )
102 101 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐷 (,) 𝐶 ) )
103 iooltub ⊢ ( ( 𝐷 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐷 (,) 𝐶 ) ) → 𝑥 < 𝐶 )
104 94 86 102 103 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 < 𝐶 )
105 85 86 89 93 104 eliood ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐵 (,) 𝐶 ) )
106 84 105 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ∧ ¬ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
107 83 106 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) )
108 107 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) → 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) )
109 80 108 impbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ↔ 𝑥 ∈ ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) )
110 109 eqrdv ⊢ ( 𝜑 → ( 𝐵 (,] 𝐶 ) = ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
111 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
112 111 a1i ⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
113 32 a1i ⊢ ( 𝜑 → ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ∈ V )
114 iooretop ⊢ ( 𝐵 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
115 114 a1i ⊢ ( 𝜑 → ( 𝐵 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) )
116 elrestr ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ∈ V ∧ ( 𝐵 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) ) → ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
117 112 113 115 116 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 (,) +∞ ) ∩ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
118 110 117 eqeltrd ⊢ ( 𝜑 → ( 𝐵 (,] 𝐶 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
119 20 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
120 119 oveq1i ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) )
121 28 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
122 ioossre ⊢ ( 𝐷 (,) 𝐶 ) ⊆ ℝ
123 16 122 sstri ⊢ ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ⊆ ℝ
124 123 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ⊆ ℝ )
125 3 snssd ⊢ ( 𝜑 → { 𝐶 } ⊆ ℝ )
126 124 125 unssd ⊢ ( 𝜑 → ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ⊆ ℝ )
127 reex ⊢ ℝ ∈ V
128 127 a1i ⊢ ( 𝜑 → ℝ ∈ V )
129 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ⊆ ℝ ∧ ℝ ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
130 121 126 128 129 syl3anc ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
131 120 130 syl5eq ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
132 118 131 eleqtrd ⊢ ( 𝜑 → ( 𝐵 (,] 𝐶 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) )
133 isopn3i ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ∈ Top ∧ ( 𝐵 (,] 𝐶 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ‘ ( 𝐵 (,] 𝐶 ) ) = ( 𝐵 (,] 𝐶 ) )
134 35 132 133 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ‘ ( 𝐵 (,] 𝐶 ) ) = ( 𝐵 (,] 𝐶 ) )
135 27 134 eqtr2d ⊢ ( 𝜑 → ( 𝐵 (,] 𝐶 ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ‘ ( ( 𝐵 (,) 𝐶 ) ∪ { 𝐶 } ) ) )
136 24 135 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∩ ( 𝐷 (,) 𝐶 ) ) ∪ { 𝐶 } ) ) ) ‘ ( ( 𝐵 (,) 𝐶 ) ∪ { 𝐶 } ) ) )
137 14 15 19 20 21 136 limcres ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( 𝐷 (,) 𝐶 ) ) ↾ ( 𝐵 (,) 𝐶 ) ) limℂ 𝐶 ) = ( ( 𝐹 ↾ ( 𝐷 (,) 𝐶 ) ) limℂ 𝐶 ) )
138 12 137 eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐵 (,) 𝐶 ) ) limℂ 𝐶 ) = ( ( 𝐹 ↾ ( 𝐷 (,) 𝐶 ) ) limℂ 𝐶 ) )