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 40605
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 23834 . . . . . . 7 (𝐹 lim 𝐴) ⊆ ℂ
3 cncfiooicclem1.r . . . . . . 7 (𝜑𝑅 ∈ (𝐹 lim 𝐴))
42, 3sseldi 3738 . . . . . 6 (𝜑𝑅 ∈ ℂ)
54ad2antrr 764 . . . . 5 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → 𝑅 ∈ ℂ)
6 limccl 23834 . . . . . . . 8 (𝐹 lim 𝐵) ⊆ ℂ
7 cncfiooicclem1.l . . . . . . . 8 (𝜑𝐿 ∈ (𝐹 lim 𝐵))
86, 7sseldi 3738 . . . . . . 7 (𝜑𝐿 ∈ ℂ)
98ad3antrrr 768 . . . . . 6 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ)
10 simplll 815 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝜑)
11 orel1 396 . . . . . . . . . . 11 𝑥 = 𝐴 → ((𝑥 = 𝐴𝑥 = 𝐵) → 𝑥 = 𝐵))
1211con3dimp 456 . . . . . . . . . 10 ((¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ (𝑥 = 𝐴𝑥 = 𝐵))
13 vex 3339 . . . . . . . . . . 11 𝑥 ∈ V
1413elpr 4339 . . . . . . . . . 10 (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴𝑥 = 𝐵))
1512, 14sylnibr 318 . . . . . . . . 9 ((¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵})
1615adantll 752 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵})
17 simpllr 817 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
18 cncfiooicclem1.a . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
1918rexrd 10277 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
2010, 19syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ∈ ℝ*)
21 cncfiooicclem1.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ)
2221rexrd 10277 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ*)
2310, 22syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ*)
24 cncfiooicclem1.altb . . . . . . . . . . . . 13 (𝜑𝐴 < 𝐵)
2518, 21, 24ltled 10373 . . . . . . . . . . . 12 (𝜑𝐴𝐵)
2610, 25syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴𝐵)
27 prunioo 12490 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
2820, 23, 26, 27syl3anc 1477 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
2917, 28eleqtrrd 2838 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}))
30 elun 3892 . . . . . . . . 9 (𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}))
3129, 30sylib 208 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}))
32 orel2 397 . . . . . . . 8 𝑥 ∈ {𝐴, 𝐵} → ((𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}) → 𝑥 ∈ (𝐴(,)𝐵)))
3316, 31, 32sylc 65 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴(,)𝐵))
34 cncfiooicclem1.f . . . . . . . . 9 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
35 cncff 22893 . . . . . . . . 9 (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
3634, 35syl 17 . . . . . . . 8 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
3736ffvelrnda 6518 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐹𝑥) ∈ ℂ)
3810, 33, 37syl2anc 696 . . . . . 6 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹𝑥) ∈ ℂ)
399, 38ifclda 4260 . . . . 5 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) ∈ ℂ)
405, 39ifclda 4260 . . . 4 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ)
41 cncfiooicclem1.g . . . 4 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
421, 40, 41fmptdf 6546 . . 3 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
43 elun 3892 . . . . . . 7 (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}))
4419, 22, 25, 27syl3anc 1477 . . . . . . . 8 (𝜑 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
4544eleq2d 2821 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
4643, 45syl5bbr 274 . . . . . 6 (𝜑 → ((𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
4746biimpar 503 . . . . 5 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}))
48 ioossicc 12448 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
49 fssres 6227 . . . . . . . . . . . . 13 ((𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
5042, 48, 49sylancl 697 . . . . . . . . . . . 12 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
5150feqmptd 6407 . . . . . . . . . . 11 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)))
52 nfmpt1 4895 . . . . . . . . . . . . . . . 16 𝑥(𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
5341, 52nfcxfr 2896 . . . . . . . . . . . . . . 15 𝑥𝐺
54 nfcv 2898 . . . . . . . . . . . . . . 15 𝑥(𝐴(,)𝐵)
5553, 54nfres 5549 . . . . . . . . . . . . . 14 𝑥(𝐺 ↾ (𝐴(,)𝐵))
56 nfcv 2898 . . . . . . . . . . . . . 14 𝑥𝑦
5755, 56nffv 6355 . . . . . . . . . . . . 13 𝑥((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)
58 nfcv 2898 . . . . . . . . . . . . . 14 𝑦(𝐺 ↾ (𝐴(,)𝐵))
59 nfcv 2898 . . . . . . . . . . . . . 14 𝑦𝑥
6058, 59nffv 6355 . . . . . . . . . . . . 13 𝑦((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)
61 fveq2 6348 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦) = ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥))
6257, 60, 61cbvmpt 4897 . . . . . . . . . . . 12 (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥))
6362a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)))
64 fvres 6364 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴(,)𝐵) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺𝑥))
6564adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺𝑥))
66 simpr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵))
6748, 66sseldi 3738 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
684adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
698ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ)
7037adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑥 = 𝐵) → (𝐹𝑥) ∈ ℂ)
7169, 70ifclda 4260 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) ∈ ℂ)
7268, 71ifcld 4271 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ)
7341fvmpt2 6449 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
7467, 72, 73syl2anc 696 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
75 elioo4g 12423 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ) ∧ (𝐴 < 𝑥𝑥 < 𝐵)))
7675biimpi 206 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴(,)𝐵) → ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ) ∧ (𝐴 < 𝑥𝑥 < 𝐵)))
7776simpld 477 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ))
7877simp1d 1137 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 ∈ ℝ*)
79 elioore 12394 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
8079rexrd 10277 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ*)
81 eliooord 12422 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑥𝑥 < 𝐵))
8281simpld 477 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 < 𝑥)
83 xrltne 12183 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ*𝑥 ∈ ℝ*𝐴 < 𝑥) → 𝑥𝐴)
8478, 80, 82, 83syl3anc 1477 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥𝐴)
8584adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥𝐴)
8685neneqd 2933 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐴)
8786iffalsed 4237 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
8881simprd 482 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 < 𝐵)
8979, 88ltned 10361 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥𝐵)
9089neneqd 2933 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴(,)𝐵) → ¬ 𝑥 = 𝐵)
9190iffalsed 4237 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴(,)𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = (𝐹𝑥))
9291adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = (𝐹𝑥))
9387, 92eqtrd 2790 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = (𝐹𝑥))
9465, 74, 933eqtrd 2794 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹𝑥))
951, 94mpteq2da 4891 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
9651, 63, 953eqtrd 2794 . . . . . . . . . 10 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
9736feqmptd 6407 . . . . . . . . . . 11 (𝜑𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
98 ioosscn 40215 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ ℂ
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
100 ssid 3761 . . . . . . . . . . . 12 ℂ ⊆ ℂ
101 eqid 2756 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
102 eqid 2756 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
103101cnfldtop 22784 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ Top
104 unicntop 22786 . . . . . . . . . . . . . . . 16 ℂ = (TopOpen‘ℂfld)
105104restid 16292 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
106103, 105ax-mp 5 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
107106eqcomi 2765 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
108101, 102, 107cncfcn 22909 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
10999, 100, 108sylancl 697 . . . . . . . . . . 11 (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
11034, 97, 1093eltr3d 2849 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
11196, 110eqeltrd 2835 . . . . . . . . 9 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
112104restuni 21164 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ ℂ) → (𝐴(,)𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
113103, 98, 112mp2an 710 . . . . . . . . . 10 (𝐴(,)𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
114113cncnpi 21280 . . . . . . . . 9 (((𝐺 ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
115111, 114sylan 489 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
116103a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (TopOpen‘ℂfld) ∈ Top)
11748a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
118 ovex 6837 . . . . . . . . . . . . 13 (𝐴[,]𝐵) ∈ V
119118a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ∈ V)
120 restabs 21167 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ∈ V) → (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
121116, 117, 119, 120syl3anc 1477 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
122121eqcomd 2762 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)))
123122oveq1d 6824 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)))
124123fveq1d 6350 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = (((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
125115, 124eleqtrd 2837 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ (((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
126 resttop 21162 . . . . . . . . . 10 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ∈ V) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top)
127103, 118, 126mp2an 710 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top
128127a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top)
12948a1i 11 . . . . . . . . . 10 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
13018, 21iccssred 40226 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
131 ax-resscn 10181 . . . . . . . . . . . 12 ℝ ⊆ ℂ
132130, 131syl6ss 3752 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
133104restuni 21164 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐴[,]𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
134103, 132, 133sylancr 698 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
135129, 134sseqtrd 3778 . . . . . . . . 9 (𝜑 → (𝐴(,)𝐵) ⊆ ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
136135adantr 472 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
137 retop 22762 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
138137a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (topGen‘ran (,)) ∈ Top)
139 ioossre 12424 . . . . . . . . . . . . . . 15 (𝐴(,)𝐵) ⊆ ℝ
140 difss 3876 . . . . . . . . . . . . . . 15 (ℝ ∖ (𝐴[,]𝐵)) ⊆ ℝ
141139, 140unssi 3927 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ
142141a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ)
143 ssun1 3915 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))
144143a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))
145 uniretop 22763 . . . . . . . . . . . . . 14 ℝ = (topGen‘ran (,))
146145ntrss 21057 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) → ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) ⊆ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
147138, 142, 144, 146syl3anc 1477 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) ⊆ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
148 simpr 479 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴(,)𝐵))
149 ioontr 40235 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵)
150148, 149syl6eleqr 2846 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)))
151147, 150sseldd 3741 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
15248, 148sseldi 3738 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴[,]𝐵))
153151, 152elind 3937 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
154130adantr 472 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ)
155 eqid 2756 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵))
156145, 155restntr 21184 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
157138, 154, 117, 156syl3anc 1477 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
158153, 157eleqtrrd 2838 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
159101tgioo2 22803 . . . . . . . . . . . . . . 15 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
160159a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ))
161160oveq1d 6824 . . . . . . . . . . . . 13 (𝜑 → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)))
162103a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (TopOpen‘ℂfld) ∈ Top)
163 reex 10215 . . . . . . . . . . . . . . 15 ℝ ∈ V
164163a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ V)
165 restabs 21167 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
166162, 130, 164, 165syl3anc 1477 . . . . . . . . . . . . 13 (𝜑 → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
167161, 166eqtrd 2790 . . . . . . . . . . . 12 (𝜑 → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
168167fveq2d 6352 . . . . . . . . . . 11 (𝜑 → (int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵))) = (int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))))
169168fveq1d 6350 . . . . . . . . . 10 (𝜑 → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
170169adantr 472 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
171158, 170eleqtrd 2837 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
172134feq2d 6188 . . . . . . . . . 10 (𝜑 → (𝐺:(𝐴[,]𝐵)⟶ℂ ↔ 𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ))
17342, 172mpbid 222 . . . . . . . . 9 (𝜑𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)
174173adantr 472 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)
175 eqid 2756 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))
176175, 104cnprest 21291 . . . . . . . 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 1478 . . . . . . 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 4338 . . . . . . 7 (𝑦 ∈ {𝐴, 𝐵} → (𝑦 = 𝐴𝑦 = 𝐵))
180 lbicc2 12477 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
18119, 22, 25, 180syl3anc 1477 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ (𝐴[,]𝐵))
182 iftrue 4232 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝑅)
183182, 41fvmptg 6438 . . . . . . . . . . . . 13 ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝑅 ∈ (𝐹 lim 𝐴)) → (𝐺𝐴) = 𝑅)
184181, 3, 183syl2anc 696 . . . . . . . . . . . 12 (𝜑 → (𝐺𝐴) = 𝑅)
18597eqcomd 2762 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) = 𝐹)
18696, 185eqtr2d 2791 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝐺 ↾ (𝐴(,)𝐵)))
187186oveq1d 6824 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 lim 𝐴) = ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴))
1883, 187eleqtrd 2837 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴))
18918, 21, 24, 42limciccioolb 40352 . . . . . . . . . . . . 13 (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴) = (𝐺 lim 𝐴))
190188, 189eleqtrd 2837 . . . . . . . . . . . 12 (𝜑𝑅 ∈ (𝐺 lim 𝐴))
191184, 190eqeltrd 2835 . . . . . . . . . . 11 (𝜑 → (𝐺𝐴) ∈ (𝐺 lim 𝐴))
192 eqid 2756 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))
193101, 192cnplimc 23846 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐴) ∈ (𝐺 lim 𝐴))))
194132, 181, 193syl2anc 696 . . . . . . . . . . 11 (𝜑 → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐴) ∈ (𝐺 lim 𝐴))))
19542, 191, 194mpbir2and 995 . . . . . . . . . 10 (𝜑𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
196195adantr 472 . . . . . . . . 9 ((𝜑𝑦 = 𝐴) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
197 fveq2 6348 . . . . . . . . . . 11 (𝑦 = 𝐴 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
198197eqcomd 2762 . . . . . . . . . 10 (𝑦 = 𝐴 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
199198adantl 473 . . . . . . . . 9 ((𝜑𝑦 = 𝐴) → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
200196, 199eleqtrd 2837 . . . . . . . 8 ((𝜑𝑦 = 𝐴) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
20121leidd 10782 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐵)
20218, 21, 21, 25, 201eliccd 40225 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐴[,]𝐵))
203 eqid 2756 . . . . . . . . . . . . . . . . . 18 𝐵 = 𝐵
204203iftruei 4233 . . . . . . . . . . . . . . . . 17 if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) = 𝐿
205204, 8syl5eqel 2839 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) ∈ ℂ)
2064, 205ifcld 4271 . . . . . . . . . . . . . . 15 (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)
207202, 206jca 555 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ))
208 nfv 1988 . . . . . . . . . . . . . . . 16 𝑥(𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)
209 nfcv 2898 . . . . . . . . . . . . . . . . . 18 𝑥𝐵
21053, 209nffv 6355 . . . . . . . . . . . . . . . . 17 𝑥(𝐺𝐵)
211210nfeq1 2912 . . . . . . . . . . . . . . . 16 𝑥(𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
212208, 211nfim 1970 . . . . . . . . . . . . . . 15 𝑥((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
213 eleq1 2823 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝐵 ∈ (𝐴[,]𝐵)))
214182adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝑅)
215 eqtr2 2776 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝐵 = 𝐴)
216 iftrue 4232 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 = 𝐴 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = 𝑅)
217216eqcomd 2762 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 = 𝐴𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
218215, 217syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
219214, 218eqtrd 2790 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝐵𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
220 iffalse 4235 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
221220adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
222 iftrue 4232 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = 𝐿)
223222adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = 𝐿)
224 df-ne 2929 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐴 ↔ ¬ 𝑥 = 𝐴)
225 pm13.18 3009 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 = 𝐵𝑥𝐴) → 𝐵𝐴)
226224, 225sylan2br 494 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐵𝐴)
227226neneqd 2933 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → ¬ 𝐵 = 𝐴)
228227iffalsed 4237 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
229228, 204syl6req 2807 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐿 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
230221, 223, 2293eqtrd 2794 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
231219, 230pm2.61dan 867 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐵 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
232231eleq1d 2820 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ ↔ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ))
233213, 232anbi12d 749 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐵 → ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) ↔ (𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)))
234 fveq2 6348 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (𝐺𝑥) = (𝐺𝐵))
235234, 231eqeq12d 2771 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐵 → ((𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ↔ (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))))
236233, 235imbi12d 333 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → (((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))) ↔ ((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))))
237212, 236, 73vtoclg1f 3401 . . . . . . . . . . . . . 14 (𝐵 ∈ (𝐴[,]𝐵) → ((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))))
238202, 207, 237sylc 65 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
23918, 24gtned 10360 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐴)
240239neneqd 2933 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐵 = 𝐴)
241240iffalsed 4237 . . . . . . . . . . . . 13 (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
242204a1i 11 . . . . . . . . . . . . 13 (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) = 𝐿)
243238, 241, 2423eqtrd 2794 . . . . . . . . . . . 12 (𝜑 → (𝐺𝐵) = 𝐿)
244186oveq1d 6824 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 lim 𝐵) = ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵))
2457, 244eleqtrd 2837 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵))
24618, 21, 24, 42limcicciooub 40368 . . . . . . . . . . . . 13 (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵) = (𝐺 lim 𝐵))
247245, 246eleqtrd 2837 . . . . . . . . . . . 12 (𝜑𝐿 ∈ (𝐺 lim 𝐵))
248243, 247eqeltrd 2835 . . . . . . . . . . 11 (𝜑 → (𝐺𝐵) ∈ (𝐺 lim 𝐵))
249101, 192cnplimc 23846 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐵 ∈ (𝐴[,]𝐵)) → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐵) ∈ (𝐺 lim 𝐵))))
250132, 202, 249syl2anc 696 . . . . . . . . . . 11 (𝜑 → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐵) ∈ (𝐺 lim 𝐵))))
25142, 248, 250mpbir2and 995 . . . . . . . . . 10 (𝜑𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
252251adantr 472 . . . . . . . . 9 ((𝜑𝑦 = 𝐵) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
253 fveq2 6348 . . . . . . . . . . 11 (𝑦 = 𝐵 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
254253eqcomd 2762 . . . . . . . . . 10 (𝑦 = 𝐵 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
255254adantl 473 . . . . . . . . 9 ((𝜑𝑦 = 𝐵) → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
256252, 255eleqtrd 2837 . . . . . . . 8 ((𝜑𝑦 = 𝐵) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
257200, 256jaodan 861 . . . . . . 7 ((𝜑 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
258179, 257sylan2 492 . . . . . 6 ((𝜑𝑦 ∈ {𝐴, 𝐵}) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
259178, 258jaodan 861 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
26047, 259syldan 488 . . . 4 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
261260ralrimiva 3100 . . 3 (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
262101cnfldtopon 22783 . . . . 5 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
263 resttopon 21163 . . . . 5 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴[,]𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)))
264262, 132, 263sylancr 698 . . . 4 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)))
265 cncnp 21282 . . . 4 ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
266264, 262, 265sylancl 697 . . 3 (𝜑 → (𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
26742, 261, 266mpbir2and 995 . 2 (𝜑𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
268101, 192, 107cncfcn 22909 . . 3 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
269132, 100, 268sylancl 697 . 2 (𝜑 → ((𝐴[,]𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
270267, 269eleqtrrd 2838 1 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1628  wnf 1853  wcel 2135  wne 2928  wral 3046  Vcvv 3336  cdif 3708  cun 3709  cin 3710  wss 3711  ifcif 4226  {cpr 4319   cuni 4584   class class class wbr 4800  cmpt 4877  ran crn 5263  cres 5264  wf 6041  cfv 6045  (class class class)co 6809  cc 10122  cr 10123  *cxr 10261   < clt 10262  cle 10263  (,)cioo 12364  [,]cicc 12367  t crest 16279  TopOpenctopn 16280  topGenctg 16296  fldccnfld 19944  Topctop 20896  TopOnctopon 20913  intcnt 21019   Cn ccn 21226   CnP ccnp 21227  cnccncf 22876   lim climc 23821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201  ax-pre-sup 10202
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-iin 4671  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-oadd 7729  df-er 7907  df-map 8021  df-pm 8022  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-fi 8478  df-sup 8509  df-inf 8510  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-nn 11209  df-2 11267  df-3 11268  df-4 11269  df-5 11270  df-6 11271  df-7 11272  df-8 11273  df-9 11274  df-n0 11481  df-z 11566  df-dec 11682  df-uz 11876  df-q 11978  df-rp 12022  df-xneg 12135  df-xadd 12136  df-xmul 12137  df-ioo 12368  df-ioc 12369  df-ico 12370  df-icc 12371  df-fz 12516  df-seq 12992  df-exp 13051  df-cj 14034  df-re 14035  df-im 14036  df-sqrt 14170  df-abs 14171  df-struct 16057  df-ndx 16058  df-slot 16059  df-base 16061  df-plusg 16152  df-mulr 16153  df-starv 16154  df-tset 16158  df-ple 16159  df-ds 16162  df-unif 16163  df-rest 16281  df-topn 16282  df-topgen 16302  df-psmet 19936  df-xmet 19937  df-met 19938  df-bl 19939  df-mopn 19940  df-cnfld 19945  df-top 20897  df-topon 20914  df-topsp 20935  df-bases 20948  df-cld 21021  df-ntr 21022  df-cls 21023  df-cn 21229  df-cnp 21230  df-xms 22322  df-ms 22323  df-cncf 22878  df-limc 23825
This theorem is referenced by:  cncfiooicc  40606
  Copyright terms: Public domain W3C validator