Metamath Proof Explorer

Theorem limciccioolb

Description: The limit of a function at the lower bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limciccioolb.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
limciccioolb.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
limciccioolb.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
limciccioolb.4 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
Assertion limciccioolb ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) = ( 𝐹 limℂ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 limciccioolb.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 limciccioolb.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 limciccioolb.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 limciccioolb.4 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
5 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
6 5 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
7 1 2 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
8 ax-resscn ⊢ ℝ ⊆ ℂ
9 7 8 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
10 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
11 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) )
12 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
13 12 a1i ⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
14 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
15 icossre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
16 1 14 15 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
17 difssd ⊢ ( 𝜑 → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ )
18 16 17 unssd ⊢ ( 𝜑 → ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ )
19 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
20 18 19 sseqtrdi ⊢ ( 𝜑 → ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ∪ ( topGen ‘ ran (,) ) )
21 elioore ⊢ ( 𝑥 ∈ ( -∞ (,) 𝐵 ) → 𝑥 ∈ ℝ )
22 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
23 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑥 )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → 𝑥 ∈ ( -∞ (,) 𝐵 ) )
25 mnfxr ⊢ -∞ ∈ ℝ*
26 25 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → -∞ ∈ ℝ* )
27 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
28 elioo2 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( -∞ (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
29 26 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → ( 𝑥 ∈ ( -∞ (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
30 24 29 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵 ) )
31 30 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → 𝑥 < 𝐵 )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝑥 < 𝐵 )
33 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ∈ ℝ )
34 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝐵 ∈ ℝ* )
35 elico2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
36 33 34 35 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
37 22 23 32 36 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
38 37 orcd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
39 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ¬ 𝐴 ≤ 𝑥 )
41 40 intnanrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ¬ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
42 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝐴 ∈ ℝ* )
44 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝐵 ∈ ℝ* )
45 39 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
46 elicc4 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
47 43 44 45 46 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
48 41 47 mtbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
49 39 48 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) )
50 49 olcd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
51 38 50 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
52 elun ⊢ ( 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ↔ ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
53 51 52 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
54 53 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( -∞ (,) 𝐵 ) 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
55 dfss3 ⊢ ( ( -∞ (,) 𝐵 ) ⊆ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ ( -∞ (,) 𝐵 ) 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
56 54 55 sylibr ⊢ ( 𝜑 → ( -∞ (,) 𝐵 ) ⊆ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
57 eqid ⊢ ∪ ( topGen ‘ ran (,) ) = ∪ ( topGen ‘ ran (,) )
58 57 ntrss ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ∪ ( topGen ‘ ran (,) ) ∧ ( -∞ (,) 𝐵 ) ⊆ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
59 13 20 56 58 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
60 25 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
61 1 mnfltd ⊢ ( 𝜑 → -∞ < 𝐴 )
62 60 14 1 61 3 eliood ⊢ ( 𝜑 → 𝐴 ∈ ( -∞ (,) 𝐵 ) )
63 iooretop ⊢ ( -∞ (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
64 63 a1i ⊢ ( 𝜑 → ( -∞ (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
65 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) = ( -∞ (,) 𝐵 ) )
66 13 64 65 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) = ( -∞ (,) 𝐵 ) )
67 62 66 eleqtrrd ⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) )
68 59 67 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
69 1 leidd ⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
70 1 2 3 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
71 1 2 1 69 70 eliccd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
72 68 71 elind ⊢ ( 𝜑 → 𝐴 ∈ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
73 icossicc ⊢ ( 𝐴 [,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
74 73 a1i ⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
75 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) )
76 19 75 restntr ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( 𝐴 [,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
77 13 7 74 76 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
78 72 77 eleqtrrd ⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) )
79 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
80 10 79 rerest ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
81 7 80 syl ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
82 81 eqcomd ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
83 82 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) )
84 83 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) )
85 78 84 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) )
86 71 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( 𝐴 [,] 𝐵 ) )
87 ssequn2 ⊢ ( { 𝐴 } ⊆ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) = ( 𝐴 [,] 𝐵 ) )
88 86 87 sylib ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) = ( 𝐴 [,] 𝐵 ) )
89 88 eqcomd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) )
90 89 oveq2d ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) )
91 90 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) ) )
92 uncom ⊢ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) = ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) )
93 snunioo ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
94 42 14 3 93 syl3anc ⊢ ( 𝜑 → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
95 92 94 eqtr2id ⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) )
96 91 95 fveq12d ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ) )
97 85 96 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ) )
98 4 6 9 10 11 97 limcres ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) = ( 𝐹 limℂ 𝐴 ) )