Metamath Proof Explorer

Theorem cncfiooicclem1

Description: A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B . F can be complex-valued. This lemma assumes A < B , the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfiooicclem1.x ⊢ Ⅎ 𝑥 𝜑
cncfiooicclem1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
cncfiooicclem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
cncfiooicclem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
cncfiooicclem1.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
cncfiooicclem1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
cncfiooicclem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
cncfiooicclem1.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
Assertion cncfiooicclem1 ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 cncfiooicclem1.x ⊢ Ⅎ 𝑥 𝜑
2 cncfiooicclem1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
3 cncfiooicclem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 cncfiooicclem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5 cncfiooicclem1.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
6 cncfiooicclem1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
7 cncfiooicclem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
8 cncfiooicclem1.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
9 limccl ⊢ ( 𝐹 limℂ 𝐴 ) ⊆ ℂ
10 9 8 sseldi ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
11 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑥 = 𝐴 ) → 𝑅 ∈ ℂ )
12 limccl ⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ
13 12 7 sseldi ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
14 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝐿 ∈ ℂ )
15 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝜑 )
16 orel1 ⊢ ( ¬ 𝑥 = 𝐴 → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 ) )
17 16 con3dimp ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵 ) → ¬ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
18 vex ⊢ 𝑥 ∈ V
19 18 elpr ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
20 17 19 sylnibr ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵 ) → ¬ 𝑥 ∈ { 𝐴 , 𝐵 } )
21 20 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ¬ 𝑥 ∈ { 𝐴 , 𝐵 } )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
23 3 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
24 15 23 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 ∈ ℝ* )
25 4 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
26 15 25 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ* )
27 3 4 5 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
28 15 27 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 ≤ 𝐵 )
29 prunioo ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
30 24 26 28 29 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
31 22 30 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) )
32 elun ⊢ ( 𝑥 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ↔ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑥 ∈ { 𝐴 , 𝐵 } ) )
33 31 32 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑥 ∈ { 𝐴 , 𝐵 } ) )
34 orel2 ⊢ ( ¬ 𝑥 ∈ { 𝐴 , 𝐵 } → ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑥 ∈ { 𝐴 , 𝐵 } ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
35 21 33 34 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
36 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
37 6 36 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
38 37 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
39 15 35 38 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
40 14 39 ifclda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
41 11 40 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ )
42 1 41 2 fmptdf ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
43 elun ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ↔ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑦 ∈ { 𝐴 , 𝐵 } ) )
44 23 25 27 29 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
45 44 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ↔ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) )
46 43 45 bitr3id ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) )
47 46 biimpar ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑦 ∈ { 𝐴 , 𝐵 } ) )
48 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
49 fssres ⊢ ( ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
50 42 48 49 sylancl ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
51 50 feqmptd ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) )
52 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
53 2 52 nfcxfr ⊢ Ⅎ 𝑥 𝐺
54 nfcv ⊢ Ⅎ 𝑥 ( 𝐴 (,) 𝐵 )
55 53 54 nfres ⊢ Ⅎ 𝑥 ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) )
56 nfcv ⊢ Ⅎ 𝑥 𝑦
57 55 56 nffv ⊢ Ⅎ 𝑥 ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 )
58 nfcv ⊢ Ⅎ 𝑦 ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) )
59 nfcv ⊢ Ⅎ 𝑦 𝑥
60 58 59 nffv ⊢ Ⅎ 𝑦 ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 )
61 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) = ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
62 57 60 61 cbvmpt ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
63 62 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
64 fvres ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
66 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
67 48 66 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
68 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ∈ ℂ )
69 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝐵 ) → 𝐿 ∈ ℂ )
70 38 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
71 69 70 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
72 68 71 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ )
73 2 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
74 67 72 73 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
75 elioo4g ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
76 75 biimpi ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
77 76 simpld ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ℝ ) )
78 77 simp1d ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 ∈ ℝ* )
79 elioore ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℝ )
80 79 rexrd ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℝ* )
81 eliooord ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
82 81 simpld ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 < 𝑥 )
83 xrltne ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ) → 𝑥 ≠ 𝐴 )
84 78 80 82 83 syl3anc ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ≠ 𝐴 )
85 84 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 𝐴 )
86 85 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 = 𝐴 )
87 86 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
88 81 simprd ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 < 𝐵 )
89 79 88 ltned ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ≠ 𝐵 )
90 89 neneqd ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑥 = 𝐵 )
91 90 iffalsed ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
92 91 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
93 87 92 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
94 65 74 93 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
95 1 94 mpteq2da ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
96 51 63 95 3eqtrd ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
97 37 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
98 ioosscn ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
99 98 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
100 ssid ⊢ ℂ ⊆ ℂ
101 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
102 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
103 101 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
104 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
105 104 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
106 103 105 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
107 106 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
108 101 102 107 cncfcn ⊢ ( ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
109 99 100 108 sylancl ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
110 6 97 109 3eltr3d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
111 96 110 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
112 104 restuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) → ( 𝐴 (,) 𝐵 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
113 103 98 112 mp2an ⊢ ( 𝐴 (,) 𝐵 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
114 113 cncnpi ⊢ ( ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
115 111 114 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
116 103 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( TopOpen ‘ ℂfld ) ∈ Top )
117 48 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
118 ovex ⊢ ( 𝐴 [,] 𝐵 ) ∈ V
119 118 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) ∈ V )
120 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐴 [,] 𝐵 ) ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
121 116 117 119 120 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
122 121 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ↾t ( 𝐴 (,) 𝐵 ) ) )
123 122 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) )
124 123 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) = ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
125 115 124 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
126 resttop ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Top )
127 103 118 126 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Top
128 127 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Top )
129 48 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
130 3 4 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
131 ax-resscn ⊢ ℝ ⊆ ℂ
132 130 131 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
133 104 restuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ) → ( 𝐴 [,] 𝐵 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
134 103 132 133 sylancr ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
135 129 134 sseqtrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
137 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
138 137 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( topGen ‘ ran (,) ) ∈ Top )
139 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
140 difss ⊢ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ
141 139 140 unssi ⊢ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ
142 141 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ )
143 ssun1 ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) )
144 143 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
145 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
146 145 ntrss ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
147 138 142 144 146 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
148 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
149 ioontr ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 )
150 148 149 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
151 147 150 sseldd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
152 48 148 sseldi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
153 151 152 elind ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
154 130 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
155 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) )
156 145 155 restntr ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
157 138 154 117 156 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
158 153 157 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
159 101 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
160 159 a1i ⊢ ( 𝜑 → ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
161 160 oveq1d ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐴 [,] 𝐵 ) ) )
162 103 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
163 reex ⊢ ℝ ∈ V
164 163 a1i ⊢ ( 𝜑 → ℝ ∈ V )
165 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ℝ ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
166 162 130 164 165 syl3anc ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
167 161 166 eqtrd ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
168 167 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) )
169 168 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
170 169 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
171 158 170 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
172 134 feq2d ⊢ ( 𝜑 → ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ↔ 𝐺 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ⟶ ℂ ) )
173 42 172 mpbid ⊢ ( 𝜑 → 𝐺 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ⟶ ℂ )
174 173 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐺 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ⟶ ℂ )
175 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) )
176 175 104 cnprest ⊢ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑦 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ∧ 𝐺 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ⟶ ℂ ) ) → ( 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) )
177 128 136 171 174 176 syl22anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) )
178 125 177 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
179 elpri ⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } → ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
180 iftrue ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
181 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
182 23 25 27 181 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
183 2 180 182 8 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = 𝑅 )
184 97 eqcomd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = 𝐹 )
185 96 184 eqtr2d ⊢ ( 𝜑 → 𝐹 = ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) )
186 185 oveq1d ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐴 ) = ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) )
187 8 186 eleqtrd ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) )
188 3 4 5 42 limciccioolb ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) = ( 𝐺 limℂ 𝐴 ) )
189 187 188 eleqtrd ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐺 limℂ 𝐴 ) )
190 183 189 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) ∈ ( 𝐺 limℂ 𝐴 ) )
191 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) )
192 101 191 cnplimc ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ( 𝐺 ‘ 𝐴 ) ∈ ( 𝐺 limℂ 𝐴 ) ) ) )
193 132 182 192 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ( 𝐺 ‘ 𝐴 ) ∈ ( 𝐺 limℂ 𝐴 ) ) ) )
194 42 190 193 mpbir2and ⊢ ( 𝜑 → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) )
195 194 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) )
196 fveq2 ⊢ ( 𝑦 = 𝐴 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) )
197 196 eqcomd ⊢ ( 𝑦 = 𝐴 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
198 197 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
199 195 198 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
200 180 adantl ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
201 eqtr2 ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐴 )
202 iftrue ⊢ ( 𝐵 = 𝐴 → if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) = 𝑅 )
203 202 eqcomd ⊢ ( 𝐵 = 𝐴 → 𝑅 = if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) )
204 201 203 syl ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑥 = 𝐴 ) → 𝑅 = if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) )
205 200 204 eqtrd ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) )
206 iffalse ⊢ ( ¬ 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
207 206 adantl ⊢ ( ( 𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
208 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = 𝐿 )
209 208 adantr ⊢ ( ( 𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = 𝐿 )
210 df-ne ⊢ ( 𝑥 ≠ 𝐴 ↔ ¬ 𝑥 = 𝐴 )
211 pm13.18 ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑥 ≠ 𝐴 ) → 𝐵 ≠ 𝐴 )
212 210 211 sylan2br ⊢ ( ( 𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴 ) → 𝐵 ≠ 𝐴 )
213 212 neneqd ⊢ ( ( 𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴 ) → ¬ 𝐵 = 𝐴 )
214 213 iffalsed ⊢ ( ( 𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) = if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) )
215 eqid ⊢ 𝐵 = 𝐵
216 215 iftruei ⊢ if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) = 𝐿
217 214 216 eqtr2di ⊢ ( ( 𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴 ) → 𝐿 = if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) )
218 207 209 217 3eqtrd ⊢ ( ( 𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) )
219 205 218 pm2.61dan ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) )
220 4 leidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
221 3 4 4 27 220 eliccd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
222 216 13 eqeltrid ⊢ ( 𝜑 → if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ )
223 10 222 ifcld ⊢ ( 𝜑 → if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) ∈ ℂ )
224 2 219 221 223 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) = if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) )
225 3 5 gtned ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
226 225 neneqd ⊢ ( 𝜑 → ¬ 𝐵 = 𝐴 )
227 226 iffalsed ⊢ ( 𝜑 → if ( 𝐵 = 𝐴 , 𝑅 , if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) ) = if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) )
228 216 a1i ⊢ ( 𝜑 → if ( 𝐵 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝐵 ) ) = 𝐿 )
229 224 227 228 3eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) = 𝐿 )
230 185 oveq1d ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) )
231 7 230 eleqtrd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) )
232 3 4 5 42 limcicciooub ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) = ( 𝐺 limℂ 𝐵 ) )
233 231 232 eleqtrd ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐺 limℂ 𝐵 ) )
234 229 233 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ( 𝐺 limℂ 𝐵 ) )
235 101 191 cnplimc ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ( 𝐺 ‘ 𝐵 ) ∈ ( 𝐺 limℂ 𝐵 ) ) ) )
236 132 221 235 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ( 𝐺 ‘ 𝐵 ) ∈ ( 𝐺 limℂ 𝐵 ) ) ) )
237 42 234 236 mpbir2and ⊢ ( 𝜑 → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) )
238 237 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) )
239 fveq2 ⊢ ( 𝑦 = 𝐵 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) )
240 239 eqcomd ⊢ ( 𝑦 = 𝐵 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
241 240 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
242 238 241 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
243 199 242 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
244 179 243 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
245 178 244 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑦 ∈ { 𝐴 , 𝐵 } ) ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
246 47 245 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
247 246 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
248 101 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
249 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
250 248 132 249 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
251 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐺 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
252 250 248 251 sylancl ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) 𝐺 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
253 42 247 252 mpbir2and ⊢ ( 𝜑 → 𝐺 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
254 101 191 107 cncfcn ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
255 132 100 254 sylancl ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
256 253 255 eleqtrrd ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )