Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cncfiooicclem1 Structured version   Visualization version   GIF version

Theorem cncfiooicclem1 39441
Description: A continuous function 𝐹 on an open interval (𝐴(,)𝐵) can be extended to a continuous function 𝐺 on the corresponding closed interval, if it has a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵. 𝐹 can be complex valued. This lemma assumes 𝐴 < 𝐵, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
cncfiooicclem1.x 𝑥𝜑
cncfiooicclem1.g 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
cncfiooicclem1.a (𝜑𝐴 ∈ ℝ)
cncfiooicclem1.b (𝜑𝐵 ∈ ℝ)
cncfiooicclem1.altb (𝜑𝐴 < 𝐵)
cncfiooicclem1.f (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
cncfiooicclem1.l (𝜑𝐿 ∈ (𝐹 lim 𝐵))
cncfiooicclem1.r (𝜑𝑅 ∈ (𝐹 lim 𝐴))
Assertion
Ref Expression
cncfiooicclem1 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝐿   𝑥,𝑅
Allowed substitution hints:   𝜑(𝑥)   𝐺(𝑥)

Proof of Theorem cncfiooicclem1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 cncfiooicclem1.x . . . 4 𝑥𝜑
2 limccl 23579 . . . . . . 7 (𝐹 lim 𝐴) ⊆ ℂ
3 cncfiooicclem1.r . . . . . . 7 (𝜑𝑅 ∈ (𝐹 lim 𝐴))
42, 3sseldi 3586 . . . . . 6 (𝜑𝑅 ∈ ℂ)
54ad2antrr 761 . . . . 5 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → 𝑅 ∈ ℂ)
6 limccl 23579 . . . . . . . 8 (𝐹 lim 𝐵) ⊆ ℂ
7 cncfiooicclem1.l . . . . . . . 8 (𝜑𝐿 ∈ (𝐹 lim 𝐵))
86, 7sseldi 3586 . . . . . . 7 (𝜑𝐿 ∈ ℂ)
98ad3antrrr 765 . . . . . 6 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ)
10 simplll 797 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝜑)
11 orel1 397 . . . . . . . . . . 11 𝑥 = 𝐴 → ((𝑥 = 𝐴𝑥 = 𝐵) → 𝑥 = 𝐵))
1211con3dimp 457 . . . . . . . . . 10 ((¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ (𝑥 = 𝐴𝑥 = 𝐵))
13 vex 3193 . . . . . . . . . . 11 𝑥 ∈ V
1413elpr 4176 . . . . . . . . . 10 (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴𝑥 = 𝐵))
1512, 14sylnibr 319 . . . . . . . . 9 ((¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵})
1615adantll 749 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵})
17 simpllr 798 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
18 cncfiooicclem1.a . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
1918rexrd 10049 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
2010, 19syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ∈ ℝ*)
21 cncfiooicclem1.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ)
2221rexrd 10049 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ*)
2310, 22syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ*)
24 cncfiooicclem1.altb . . . . . . . . . . . . 13 (𝜑𝐴 < 𝐵)
2518, 21, 24ltled 10145 . . . . . . . . . . . 12 (𝜑𝐴𝐵)
2610, 25syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴𝐵)
27 prunioo 12259 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
2820, 23, 26, 27syl3anc 1323 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
2917, 28eleqtrrd 2701 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}))
30 elun 3737 . . . . . . . . 9 (𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}))
3129, 30sylib 208 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}))
32 orel2 398 . . . . . . . 8 𝑥 ∈ {𝐴, 𝐵} → ((𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}) → 𝑥 ∈ (𝐴(,)𝐵)))
3316, 31, 32sylc 65 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴(,)𝐵))
34 cncfiooicclem1.f . . . . . . . . 9 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
35 cncff 22636 . . . . . . . . 9 (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
3634, 35syl 17 . . . . . . . 8 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
3736ffvelrnda 6325 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐹𝑥) ∈ ℂ)
3810, 33, 37syl2anc 692 . . . . . 6 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹𝑥) ∈ ℂ)
399, 38ifclda 4098 . . . . 5 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) ∈ ℂ)
405, 39ifclda 4098 . . . 4 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ)
41 cncfiooicclem1.g . . . 4 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
421, 40, 41fmptdf 6353 . . 3 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
43 elun 3737 . . . . . . 7 (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}))
4419, 22, 25, 27syl3anc 1323 . . . . . . . 8 (𝜑 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
4544eleq2d 2684 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
4643, 45syl5bbr 274 . . . . . 6 (𝜑 → ((𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
4746biimpar 502 . . . . 5 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}))
48 ioossicc 12217 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
49 fssres 6037 . . . . . . . . . . . . 13 ((𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
5042, 48, 49sylancl 693 . . . . . . . . . . . 12 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
5150feqmptd 6216 . . . . . . . . . . 11 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)))
52 nfmpt1 4717 . . . . . . . . . . . . . . . 16 𝑥(𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
5341, 52nfcxfr 2759 . . . . . . . . . . . . . . 15 𝑥𝐺
54 nfcv 2761 . . . . . . . . . . . . . . 15 𝑥(𝐴(,)𝐵)
5553, 54nfres 5368 . . . . . . . . . . . . . 14 𝑥(𝐺 ↾ (𝐴(,)𝐵))
56 nfcv 2761 . . . . . . . . . . . . . 14 𝑥𝑦
5755, 56nffv 6165 . . . . . . . . . . . . 13 𝑥((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)
58 nfcv 2761 . . . . . . . . . . . . . 14 𝑦(𝐺 ↾ (𝐴(,)𝐵))
59 nfcv 2761 . . . . . . . . . . . . . 14 𝑦𝑥
6058, 59nffv 6165 . . . . . . . . . . . . 13 𝑦((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)
61 fveq2 6158 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦) = ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥))
6257, 60, 61cbvmpt 4719 . . . . . . . . . . . 12 (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥))
6362a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)))
64 fvres 6174 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴(,)𝐵) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺𝑥))
6564adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺𝑥))
66 simpr 477 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵))
6748, 66sseldi 3586 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
684adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
698ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ)
7037adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑥 = 𝐵) → (𝐹𝑥) ∈ ℂ)
7169, 70ifclda 4098 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) ∈ ℂ)
7268, 71ifcld 4109 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ)
7341fvmpt2 6258 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
7467, 72, 73syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
75 elioo4g 12192 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ) ∧ (𝐴 < 𝑥𝑥 < 𝐵)))
7675biimpi 206 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴(,)𝐵) → ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ) ∧ (𝐴 < 𝑥𝑥 < 𝐵)))
7776simpld 475 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ))
7877simp1d 1071 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 ∈ ℝ*)
79 elioore 12163 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
8079rexrd 10049 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ*)
81 eliooord 12191 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑥𝑥 < 𝐵))
8281simpld 475 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 < 𝑥)
83 xrltne 11954 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ*𝑥 ∈ ℝ*𝐴 < 𝑥) → 𝑥𝐴)
8478, 80, 82, 83syl3anc 1323 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥𝐴)
8584adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥𝐴)
8685neneqd 2795 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐴)
8786iffalsed 4075 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
8881simprd 479 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 < 𝐵)
8979, 88ltned 10133 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥𝐵)
9089neneqd 2795 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴(,)𝐵) → ¬ 𝑥 = 𝐵)
9190iffalsed 4075 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴(,)𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = (𝐹𝑥))
9291adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = (𝐹𝑥))
9387, 92eqtrd 2655 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = (𝐹𝑥))
9465, 74, 933eqtrd 2659 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹𝑥))
951, 94mpteq2da 4713 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
9651, 63, 953eqtrd 2659 . . . . . . . . . 10 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
9736feqmptd 6216 . . . . . . . . . . 11 (𝜑𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
98 ioosscn 39162 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ ℂ
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
100 ssid 3609 . . . . . . . . . . . 12 ℂ ⊆ ℂ
101 eqid 2621 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
102 eqid 2621 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
103101cnfldtop 22527 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ Top
104 unicntop 22529 . . . . . . . . . . . . . . . 16 ℂ = (TopOpen‘ℂfld)
105104restid 16034 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
106103, 105ax-mp 5 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
107106eqcomi 2630 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
108101, 102, 107cncfcn 22652 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
10999, 100, 108sylancl 693 . . . . . . . . . . 11 (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
11034, 97, 1093eltr3d 2712 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
11196, 110eqeltrd 2698 . . . . . . . . 9 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
112104restuni 20906 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ ℂ) → (𝐴(,)𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
113103, 98, 112mp2an 707 . . . . . . . . . 10 (𝐴(,)𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
114113cncnpi 21022 . . . . . . . . 9 (((𝐺 ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
115111, 114sylan 488 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
116103a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (TopOpen‘ℂfld) ∈ Top)
11748a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
118 ovex 6643 . . . . . . . . . . . . 13 (𝐴[,]𝐵) ∈ V
119118a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ∈ V)
120 restabs 20909 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ∈ V) → (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
121116, 117, 119, 120syl3anc 1323 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
122121eqcomd 2627 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)))
123122oveq1d 6630 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)))
124123fveq1d 6160 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = (((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
125115, 124eleqtrd 2700 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ (((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
126 resttop 20904 . . . . . . . . . 10 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ∈ V) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top)
127103, 118, 126mp2an 707 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top
128127a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top)
12948a1i 11 . . . . . . . . . 10 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
13018, 21iccssred 39173 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
131 ax-resscn 9953 . . . . . . . . . . . 12 ℝ ⊆ ℂ
132130, 131syl6ss 3600 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
133104restuni 20906 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐴[,]𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
134103, 132, 133sylancr 694 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
135129, 134sseqtrd 3626 . . . . . . . . 9 (𝜑 → (𝐴(,)𝐵) ⊆ ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
136135adantr 481 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
137 retop 22505 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
138137a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (topGen‘ran (,)) ∈ Top)
139 ioossre 12193 . . . . . . . . . . . . . . 15 (𝐴(,)𝐵) ⊆ ℝ
140 difss 3721 . . . . . . . . . . . . . . 15 (ℝ ∖ (𝐴[,]𝐵)) ⊆ ℝ
141139, 140unssi 3772 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ
142141a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ)
143 ssun1 3760 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))
144143a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))
145 uniretop 22506 . . . . . . . . . . . . . 14 ℝ = (topGen‘ran (,))
146145ntrss 20799 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) → ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) ⊆ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
147138, 142, 144, 146syl3anc 1323 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) ⊆ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
148 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴(,)𝐵))
149 ioontr 39182 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵)
150148, 149syl6eleqr 2709 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)))
151147, 150sseldd 3589 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
15248, 148sseldi 3586 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴[,]𝐵))
153151, 152elind 3782 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
154130adantr 481 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ)
155 eqid 2621 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵))
156145, 155restntr 20926 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
157138, 154, 117, 156syl3anc 1323 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
158153, 157eleqtrrd 2701 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
159101tgioo2 22546 . . . . . . . . . . . . . . 15 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
160159a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ))
161160oveq1d 6630 . . . . . . . . . . . . 13 (𝜑 → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)))
162103a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (TopOpen‘ℂfld) ∈ Top)
163 reex 9987 . . . . . . . . . . . . . . 15 ℝ ∈ V
164163a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ V)
165 restabs 20909 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
166162, 130, 164, 165syl3anc 1323 . . . . . . . . . . . . 13 (𝜑 → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
167161, 166eqtrd 2655 . . . . . . . . . . . 12 (𝜑 → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
168167fveq2d 6162 . . . . . . . . . . 11 (𝜑 → (int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵))) = (int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))))
169168fveq1d 6160 . . . . . . . . . 10 (𝜑 → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
170169adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
171158, 170eleqtrd 2700 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
172134feq2d 5998 . . . . . . . . . 10 (𝜑 → (𝐺:(𝐴[,]𝐵)⟶ℂ ↔ 𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ))
17342, 172mpbid 222 . . . . . . . . 9 (𝜑𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)
174173adantr 481 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)
175 eqid 2621 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))
176175, 104cnprest 21033 . . . . . . . 8 (((((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))‘𝑦)))
177128, 136, 171, 174, 176syl22anc 1324 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝐺 ↾ (𝐴(,)𝐵)) ∈ (((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
178125, 177mpbird 247 . . . . . 6 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
179 elpri 4175 . . . . . . 7 (𝑦 ∈ {𝐴, 𝐵} → (𝑦 = 𝐴𝑦 = 𝐵))
180 lbicc2 12246 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
18119, 22, 25, 180syl3anc 1323 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ (𝐴[,]𝐵))
182 iftrue 4070 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝑅)
183182, 41fvmptg 6247 . . . . . . . . . . . . 13 ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝑅 ∈ (𝐹 lim 𝐴)) → (𝐺𝐴) = 𝑅)
184181, 3, 183syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (𝐺𝐴) = 𝑅)
18597eqcomd 2627 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) = 𝐹)
18696, 185eqtr2d 2656 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝐺 ↾ (𝐴(,)𝐵)))
187186oveq1d 6630 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 lim 𝐴) = ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴))
1883, 187eleqtrd 2700 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴))
18918, 21, 24, 42limciccioolb 39289 . . . . . . . . . . . . 13 (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴) = (𝐺 lim 𝐴))
190188, 189eleqtrd 2700 . . . . . . . . . . . 12 (𝜑𝑅 ∈ (𝐺 lim 𝐴))
191184, 190eqeltrd 2698 . . . . . . . . . . 11 (𝜑 → (𝐺𝐴) ∈ (𝐺 lim 𝐴))
192 eqid 2621 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))
193101, 192cnplimc 23591 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐴) ∈ (𝐺 lim 𝐴))))
194132, 181, 193syl2anc 692 . . . . . . . . . . 11 (𝜑 → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐴) ∈ (𝐺 lim 𝐴))))
19542, 191, 194mpbir2and 956 . . . . . . . . . 10 (𝜑𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
196195adantr 481 . . . . . . . . 9 ((𝜑𝑦 = 𝐴) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
197 fveq2 6158 . . . . . . . . . . 11 (𝑦 = 𝐴 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
198197eqcomd 2627 . . . . . . . . . 10 (𝑦 = 𝐴 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
199198adantl 482 . . . . . . . . 9 ((𝜑𝑦 = 𝐴) → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
200196, 199eleqtrd 2700 . . . . . . . 8 ((𝜑𝑦 = 𝐴) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
20121leidd 10554 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐵)
20218, 21, 21, 25, 201eliccd 39172 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐴[,]𝐵))
203 eqid 2621 . . . . . . . . . . . . . . . . . 18 𝐵 = 𝐵
204203iftruei 4071 . . . . . . . . . . . . . . . . 17 if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) = 𝐿
205204, 8syl5eqel 2702 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) ∈ ℂ)
2064, 205ifcld 4109 . . . . . . . . . . . . . . 15 (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)
207202, 206jca 554 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ))
208 nfv 1840 . . . . . . . . . . . . . . . 16 𝑥(𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)
209 nfcv 2761 . . . . . . . . . . . . . . . . . 18 𝑥𝐵
21053, 209nffv 6165 . . . . . . . . . . . . . . . . 17 𝑥(𝐺𝐵)
211210nfeq1 2774 . . . . . . . . . . . . . . . 16 𝑥(𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
212208, 211nfim 1822 . . . . . . . . . . . . . . 15 𝑥((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
213 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝐵 ∈ (𝐴[,]𝐵)))
214182adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝑅)
215 eqtr2 2641 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝐵 = 𝐴)
216 iftrue 4070 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 = 𝐴 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = 𝑅)
217216eqcomd 2627 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 = 𝐴𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
218215, 217syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
219214, 218eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝐵𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
220 iffalse 4073 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
221220adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
222 iftrue 4070 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = 𝐿)
223222adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = 𝐿)
224 df-ne 2791 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐴 ↔ ¬ 𝑥 = 𝐴)
225 pm13.18 2871 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 = 𝐵𝑥𝐴) → 𝐵𝐴)
226224, 225sylan2br 493 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐵𝐴)
227226neneqd 2795 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → ¬ 𝐵 = 𝐴)
228227iffalsed 4075 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
229228, 204syl6req 2672 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐿 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
230221, 223, 2293eqtrd 2659 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
231219, 230pm2.61dan 831 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐵 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
232231eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ ↔ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ))
233213, 232anbi12d 746 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐵 → ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) ↔ (𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)))
234 fveq2 6158 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (𝐺𝑥) = (𝐺𝐵))
235234, 231eqeq12d 2636 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐵 → ((𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ↔ (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))))
236233, 235imbi12d 334 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → (((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))) ↔ ((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))))
237212, 236, 73vtoclg1f 3255 . . . . . . . . . . . . . 14 (𝐵 ∈ (𝐴[,]𝐵) → ((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))))
238202, 207, 237sylc 65 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
23918, 24gtned 10132 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐴)
240239neneqd 2795 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐵 = 𝐴)
241240iffalsed 4075 . . . . . . . . . . . . 13 (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
242204a1i 11 . . . . . . . . . . . . 13 (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) = 𝐿)
243238, 241, 2423eqtrd 2659 . . . . . . . . . . . 12 (𝜑 → (𝐺𝐵) = 𝐿)
244186oveq1d 6630 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 lim 𝐵) = ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵))
2457, 244eleqtrd 2700 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵))
24618, 21, 24, 42limcicciooub 39305 . . . . . . . . . . . . 13 (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵) = (𝐺 lim 𝐵))
247245, 246eleqtrd 2700 . . . . . . . . . . . 12 (𝜑𝐿 ∈ (𝐺 lim 𝐵))
248243, 247eqeltrd 2698 . . . . . . . . . . 11 (𝜑 → (𝐺𝐵) ∈ (𝐺 lim 𝐵))
249101, 192cnplimc 23591 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐵 ∈ (𝐴[,]𝐵)) → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐵) ∈ (𝐺 lim 𝐵))))
250132, 202, 249syl2anc 692 . . . . . . . . . . 11 (𝜑 → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐵) ∈ (𝐺 lim 𝐵))))
25142, 248, 250mpbir2and 956 . . . . . . . . . 10 (𝜑𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
252251adantr 481 . . . . . . . . 9 ((𝜑𝑦 = 𝐵) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
253 fveq2 6158 . . . . . . . . . . 11 (𝑦 = 𝐵 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
254253eqcomd 2627 . . . . . . . . . 10 (𝑦 = 𝐵 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
255254adantl 482 . . . . . . . . 9 ((𝜑𝑦 = 𝐵) → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
256252, 255eleqtrd 2700 . . . . . . . 8 ((𝜑𝑦 = 𝐵) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
257200, 256jaodan 825 . . . . . . 7 ((𝜑 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
258179, 257sylan2 491 . . . . . 6 ((𝜑𝑦 ∈ {𝐴, 𝐵}) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
259178, 258jaodan 825 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
26047, 259syldan 487 . . . 4 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
261260ralrimiva 2962 . . 3 (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
262101cnfldtopon 22526 . . . . 5 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
263 resttopon 20905 . . . . 5 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴[,]𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)))
264262, 132, 263sylancr 694 . . . 4 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)))
265 cncnp 21024 . . . 4 ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
266264, 262, 265sylancl 693 . . 3 (𝜑 → (𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
26742, 261, 266mpbir2and 956 . 2 (𝜑𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
268101, 192, 107cncfcn 22652 . . 3 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
269132, 100, 268sylancl 693 . 2 (𝜑 → ((𝐴[,]𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
270267, 269eleqtrrd 2701 1 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wnf 1705  wcel 1987  wne 2790  wral 2908  Vcvv 3190  cdif 3557  cun 3558  cin 3559  wss 3560  ifcif 4064  {cpr 4157   cuni 4409   class class class wbr 4623  cmpt 4683  ran crn 5085  cres 5086  wf 5853  cfv 5857  (class class class)co 6615  cc 9894  cr 9895  *cxr 10033   < clt 10034  cle 10035  (,)cioo 12133  [,]cicc 12136  t crest 16021  TopOpenctopn 16022  topGenctg 16038  fldccnfld 19686  Topctop 20638  TopOnctopon 20655  intcnt 20761   Cn ccn 20968   CnP ccnp 20969  cnccncf 22619   lim climc 23566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fi 8277  df-sup 8308  df-inf 8309  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ioo 12137  df-ioc 12138  df-ico 12139  df-icc 12140  df-fz 12285  df-seq 12758  df-exp 12817  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-plusg 15894  df-mulr 15895  df-starv 15896  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-rest 16023  df-topn 16024  df-topgen 16044  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-cn 20971  df-cnp 20972  df-xms 22065  df-ms 22066  df-cncf 22621  df-limc 23570
This theorem is referenced by:  cncfiooicc  39442
  Copyright terms: Public domain W3C validator