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 40591
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 23863 . . . . . . 7 (𝐹 lim 𝐴) ⊆ ℂ
3 cncfiooicclem1.r . . . . . . 7 (𝜑𝑅 ∈ (𝐹 lim 𝐴))
42, 3sseldi 3807 . . . . . 6 (𝜑𝑅 ∈ ℂ)
54ad2antrr 708 . . . . 5 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → 𝑅 ∈ ℂ)
6 limccl 23863 . . . . . . . 8 (𝐹 lim 𝐵) ⊆ ℂ
7 cncfiooicclem1.l . . . . . . . 8 (𝜑𝐿 ∈ (𝐹 lim 𝐵))
86, 7sseldi 3807 . . . . . . 7 (𝜑𝐿 ∈ ℂ)
98ad3antrrr 712 . . . . . 6 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ)
10 simplll 782 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝜑)
11 orel1 904 . . . . . . . . . . 11 𝑥 = 𝐴 → ((𝑥 = 𝐴𝑥 = 𝐵) → 𝑥 = 𝐵))
1211con3dimp 397 . . . . . . . . . 10 ((¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ (𝑥 = 𝐴𝑥 = 𝐵))
13 vex 3405 . . . . . . . . . . 11 𝑥 ∈ V
1413elpr 4404 . . . . . . . . . 10 (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴𝑥 = 𝐵))
1512, 14sylnibr 320 . . . . . . . . 9 ((¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵})
1615adantll 696 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵})
17 simpllr 784 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
18 cncfiooicclem1.a . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
1918rexrd 10381 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
2010, 19syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ∈ ℝ*)
21 cncfiooicclem1.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ)
2221rexrd 10381 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ*)
2310, 22syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ*)
24 cncfiooicclem1.altb . . . . . . . . . . . . 13 (𝜑𝐴 < 𝐵)
2518, 21, 24ltled 10477 . . . . . . . . . . . 12 (𝜑𝐴𝐵)
2610, 25syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴𝐵)
27 prunioo 12531 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
2820, 23, 26, 27syl3anc 1483 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
2917, 28eleqtrrd 2899 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}))
30 elun 3963 . . . . . . . . 9 (𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}))
3129, 30sylib 209 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}))
32 orel2 906 . . . . . . . 8 𝑥 ∈ {𝐴, 𝐵} → ((𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}) → 𝑥 ∈ (𝐴(,)𝐵)))
3316, 31, 32sylc 65 . . . . . . 7 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴(,)𝐵))
34 cncfiooicclem1.f . . . . . . . . 9 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
35 cncff 22917 . . . . . . . . 9 (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
3634, 35syl 17 . . . . . . . 8 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
3736ffvelrnda 6588 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐹𝑥) ∈ ℂ)
3810, 33, 37syl2anc 575 . . . . . 6 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹𝑥) ∈ ℂ)
399, 38ifclda 4324 . . . . 5 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) ∈ ℂ)
405, 39ifclda 4324 . . . 4 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ)
41 cncfiooicclem1.g . . . 4 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
421, 40, 41fmptdf 6616 . . 3 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
43 elun 3963 . . . . . . 7 (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}))
4419, 22, 25, 27syl3anc 1483 . . . . . . . 8 (𝜑 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
4544eleq2d 2882 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
4643, 45syl5bbr 276 . . . . . 6 (𝜑 → ((𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
4746biimpar 465 . . . . 5 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}))
48 ioossicc 12484 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
49 fssres 6292 . . . . . . . . . . . . 13 ((𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
5042, 48, 49sylancl 576 . . . . . . . . . . . 12 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
5150feqmptd 6477 . . . . . . . . . . 11 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)))
52 nfmpt1 4952 . . . . . . . . . . . . . . . 16 𝑥(𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
5341, 52nfcxfr 2957 . . . . . . . . . . . . . . 15 𝑥𝐺
54 nfcv 2959 . . . . . . . . . . . . . . 15 𝑥(𝐴(,)𝐵)
5553, 54nfres 5610 . . . . . . . . . . . . . 14 𝑥(𝐺 ↾ (𝐴(,)𝐵))
56 nfcv 2959 . . . . . . . . . . . . . 14 𝑥𝑦
5755, 56nffv 6425 . . . . . . . . . . . . 13 𝑥((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)
58 nfcv 2959 . . . . . . . . . . . . . 14 𝑦(𝐺 ↾ (𝐴(,)𝐵))
59 nfcv 2959 . . . . . . . . . . . . . 14 𝑦𝑥
6058, 59nffv 6425 . . . . . . . . . . . . 13 𝑦((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)
61 fveq2 6415 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦) = ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥))
6257, 60, 61cbvmpt 4954 . . . . . . . . . . . 12 (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥))
6362a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)))
64 fvres 6434 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴(,)𝐵) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺𝑥))
6564adantl 469 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺𝑥))
66 simpr 473 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵))
6748, 66sseldi 3807 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
684adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
698ad2antrr 708 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ)
7037adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑥 = 𝐵) → (𝐹𝑥) ∈ ℂ)
7169, 70ifclda 4324 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) ∈ ℂ)
7268, 71ifcld 4335 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ)
7341fvmpt2 6519 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
7467, 72, 73syl2anc 575 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
75 elioo4g 12459 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ) ∧ (𝐴 < 𝑥𝑥 < 𝐵)))
7675biimpi 207 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴(,)𝐵) → ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ) ∧ (𝐴 < 𝑥𝑥 < 𝐵)))
7776simpld 484 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ℝ))
7877simp1d 1165 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 ∈ ℝ*)
79 elioore 12430 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
8079rexrd 10381 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ*)
81 eliooord 12458 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑥𝑥 < 𝐵))
8281simpld 484 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 < 𝑥)
83 xrltne 12219 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ*𝑥 ∈ ℝ*𝐴 < 𝑥) → 𝑥𝐴)
8478, 80, 82, 83syl3anc 1483 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥𝐴)
8584adantl 469 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥𝐴)
8685neneqd 2994 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐴)
8786iffalsed 4301 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
8881simprd 485 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 < 𝐵)
8979, 88ltned 10465 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥𝐵)
9089neneqd 2994 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴(,)𝐵) → ¬ 𝑥 = 𝐵)
9190iffalsed 4301 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴(,)𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = (𝐹𝑥))
9291adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = (𝐹𝑥))
9387, 92eqtrd 2851 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = (𝐹𝑥))
9465, 74, 933eqtrd 2855 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹𝑥))
951, 94mpteq2da 4948 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
9651, 63, 953eqtrd 2855 . . . . . . . . . 10 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
9736feqmptd 6477 . . . . . . . . . . 11 (𝜑𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
98 ioosscn 40205 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ ℂ
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
100 ssid 3831 . . . . . . . . . . . 12 ℂ ⊆ ℂ
101 eqid 2817 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
102 eqid 2817 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
103101cnfldtop 22808 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ Top
104 unicntop 22810 . . . . . . . . . . . . . . . 16 ℂ = (TopOpen‘ℂfld)
105104restid 16306 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
106103, 105ax-mp 5 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
107106eqcomi 2826 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
108101, 102, 107cncfcn 22933 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
10999, 100, 108sylancl 576 . . . . . . . . . . 11 (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
11034, 97, 1093eltr3d 2910 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
11196, 110eqeltrd 2896 . . . . . . . . 9 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
112104restuni 21188 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ ℂ) → (𝐴(,)𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
113103, 98, 112mp2an 675 . . . . . . . . . 10 (𝐴(,)𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
114113cncnpi 21304 . . . . . . . . 9 (((𝐺 ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
115111, 114sylan 571 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
116103a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (TopOpen‘ℂfld) ∈ Top)
11748a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
118 ovex 6913 . . . . . . . . . . . . 13 (𝐴[,]𝐵) ∈ V
119118a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ∈ V)
120 restabs 21191 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ∈ V) → (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
121116, 117, 119, 120syl3anc 1483 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
122121eqcomd 2823 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)))
123122oveq1d 6896 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)))
124123fveq1d 6417 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = (((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
125115, 124eleqtrd 2898 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈ (((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
126 resttop 21186 . . . . . . . . . 10 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ∈ V) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top)
127103, 118, 126mp2an 675 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top
128127a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top)
12948a1i 11 . . . . . . . . . 10 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
13018, 21iccssred 40216 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
131 ax-resscn 10285 . . . . . . . . . . . 12 ℝ ⊆ ℂ
132130, 131syl6ss 3821 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
133104restuni 21188 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐴[,]𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
134103, 132, 133sylancr 577 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
135129, 134sseqtrd 3849 . . . . . . . . 9 (𝜑 → (𝐴(,)𝐵) ⊆ ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
136135adantr 468 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
137 retop 22786 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
138137a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (topGen‘ran (,)) ∈ Top)
139 ioossre 12460 . . . . . . . . . . . . . . 15 (𝐴(,)𝐵) ⊆ ℝ
140 difss 3947 . . . . . . . . . . . . . . 15 (ℝ ∖ (𝐴[,]𝐵)) ⊆ ℝ
141139, 140unssi 3998 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ
142141a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ)
143 ssun1 3986 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))
144143a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))
145 uniretop 22787 . . . . . . . . . . . . . 14 ℝ = (topGen‘ran (,))
146145ntrss 21081 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) → ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) ⊆ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
147138, 142, 144, 146syl3anc 1483 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) ⊆ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
148 simpr 473 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴(,)𝐵))
149 ioontr 40223 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵)
150148, 149syl6eleqr 2907 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)))
151147, 150sseldd 3810 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))))
15248, 148sseldi 3807 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴[,]𝐵))
153151, 152elind 4008 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
154130adantr 468 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ)
155 eqid 2817 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵))
156145, 155restntr 21208 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
157138, 154, 117, 156syl3anc 1483 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵)))
158153, 157eleqtrrd 2899 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
159101tgioo2 22827 . . . . . . . . . . . . . . 15 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
160159a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ))
161160oveq1d 6896 . . . . . . . . . . . . 13 (𝜑 → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)))
162103a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (TopOpen‘ℂfld) ∈ Top)
163 reex 10319 . . . . . . . . . . . . . . 15 ℝ ∈ V
164163a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ V)
165 restabs 21191 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
166162, 130, 164, 165syl3anc 1483 . . . . . . . . . . . . 13 (𝜑 → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
167161, 166eqtrd 2851 . . . . . . . . . . . 12 (𝜑 → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
168167fveq2d 6419 . . . . . . . . . . 11 (𝜑 → (int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵))) = (int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))))
169168fveq1d 6417 . . . . . . . . . 10 (𝜑 → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
170169adantr 468 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
171158, 170eleqtrd 2898 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)))
172134feq2d 6249 . . . . . . . . . 10 (𝜑 → (𝐺:(𝐴[,]𝐵)⟶ℂ ↔ 𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ))
17342, 172mpbid 223 . . . . . . . . 9 (𝜑𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)
174173adantr 468 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝐺: ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)
175 eqid 2817 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))
176175, 104cnprest 21315 . . . . . . . 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 858 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝐺 ↾ (𝐴(,)𝐵)) ∈ (((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
178125, 177mpbird 248 . . . . . 6 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
179 elpri 4403 . . . . . . 7 (𝑦 ∈ {𝐴, 𝐵} → (𝑦 = 𝐴𝑦 = 𝐵))
180 lbicc2 12515 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
18119, 22, 25, 180syl3anc 1483 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ (𝐴[,]𝐵))
182 iftrue 4296 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝑅)
183182, 41fvmptg 6508 . . . . . . . . . . . . 13 ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝑅 ∈ (𝐹 lim 𝐴)) → (𝐺𝐴) = 𝑅)
184181, 3, 183syl2anc 575 . . . . . . . . . . . 12 (𝜑 → (𝐺𝐴) = 𝑅)
18597eqcomd 2823 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) = 𝐹)
18696, 185eqtr2d 2852 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝐺 ↾ (𝐴(,)𝐵)))
187186oveq1d 6896 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 lim 𝐴) = ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴))
1883, 187eleqtrd 2898 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴))
18918, 21, 24, 42limciccioolb 40338 . . . . . . . . . . . . 13 (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐴) = (𝐺 lim 𝐴))
190188, 189eleqtrd 2898 . . . . . . . . . . . 12 (𝜑𝑅 ∈ (𝐺 lim 𝐴))
191184, 190eqeltrd 2896 . . . . . . . . . . 11 (𝜑 → (𝐺𝐴) ∈ (𝐺 lim 𝐴))
192 eqid 2817 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))
193101, 192cnplimc 23875 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐴) ∈ (𝐺 lim 𝐴))))
194132, 181, 193syl2anc 575 . . . . . . . . . . 11 (𝜑 → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐴) ∈ (𝐺 lim 𝐴))))
19542, 191, 194mpbir2and 695 . . . . . . . . . 10 (𝜑𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
196195adantr 468 . . . . . . . . 9 ((𝜑𝑦 = 𝐴) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
197 fveq2 6415 . . . . . . . . . . 11 (𝑦 = 𝐴 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴))
198197eqcomd 2823 . . . . . . . . . 10 (𝑦 = 𝐴 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
199198adantl 469 . . . . . . . . 9 ((𝜑𝑦 = 𝐴) → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
200196, 199eleqtrd 2898 . . . . . . . 8 ((𝜑𝑦 = 𝐴) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
20121leidd 10886 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐵)
20218, 21, 21, 25, 201eliccd 40215 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐴[,]𝐵))
203 eqid 2817 . . . . . . . . . . . . . . . . . 18 𝐵 = 𝐵
204203iftruei 4297 . . . . . . . . . . . . . . . . 17 if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) = 𝐿
205204, 8syl5eqel 2900 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) ∈ ℂ)
2064, 205ifcld 4335 . . . . . . . . . . . . . . 15 (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)
207202, 206jca 503 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ))
208 nfv 2005 . . . . . . . . . . . . . . . 16 𝑥(𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)
209 nfcv 2959 . . . . . . . . . . . . . . . . . 18 𝑥𝐵
21053, 209nffv 6425 . . . . . . . . . . . . . . . . 17 𝑥(𝐺𝐵)
211210nfeq1 2973 . . . . . . . . . . . . . . . 16 𝑥(𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
212208, 211nfim 1987 . . . . . . . . . . . . . . 15 𝑥((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
213 eleq1 2884 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝐵 ∈ (𝐴[,]𝐵)))
214182adantl 469 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝑅)
215 eqtr2 2837 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝐵 = 𝐴)
216 iftrue 4296 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 = 𝐴 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = 𝑅)
217216eqcomd 2823 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 = 𝐴𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
218215, 217syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
219214, 218eqtrd 2851 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝐵𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
220 iffalse 4299 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
221220adantl 469 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
222 iftrue 4296 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = 𝐿)
223222adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = 𝐿)
224 df-ne 2990 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐴 ↔ ¬ 𝑥 = 𝐴)
225 pm13.18 3070 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 = 𝐵𝑥𝐴) → 𝐵𝐴)
226224, 225sylan2br 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐵𝐴)
227226neneqd 2994 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → ¬ 𝐵 = 𝐴)
228227iffalsed 4301 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
229228, 204syl6req 2868 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐿 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
230221, 223, 2293eqtrd 2855 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
231219, 230pm2.61dan 838 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐵 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
232231eleq1d 2881 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ ↔ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ))
233213, 232anbi12d 618 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐵 → ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) ↔ (𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ)))
234 fveq2 6415 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (𝐺𝑥) = (𝐺𝐵))
235234, 231eqeq12d 2832 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐵 → ((𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ↔ (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))))
236233, 235imbi12d 335 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → (((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) ∈ ℂ) → (𝐺𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))) ↔ ((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))))
237212, 236, 73vtoclg1f 3469 . . . . . . . . . . . . . 14 (𝐵 ∈ (𝐴[,]𝐵) → ((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) ∈ ℂ) → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))))
238202, 207, 237sylc 65 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))))
23918, 24gtned 10464 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐴)
240239neneqd 2994 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐵 = 𝐴)
241240iffalsed 4301 . . . . . . . . . . . . 13 (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)))
242204a1i 11 . . . . . . . . . . . . 13 (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹𝐵)) = 𝐿)
243238, 241, 2423eqtrd 2855 . . . . . . . . . . . 12 (𝜑 → (𝐺𝐵) = 𝐿)
244186oveq1d 6896 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 lim 𝐵) = ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵))
2457, 244eleqtrd 2898 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵))
24618, 21, 24, 42limcicciooub 40354 . . . . . . . . . . . . 13 (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) lim 𝐵) = (𝐺 lim 𝐵))
247245, 246eleqtrd 2898 . . . . . . . . . . . 12 (𝜑𝐿 ∈ (𝐺 lim 𝐵))
248243, 247eqeltrd 2896 . . . . . . . . . . 11 (𝜑 → (𝐺𝐵) ∈ (𝐺 lim 𝐵))
249101, 192cnplimc 23875 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐵 ∈ (𝐴[,]𝐵)) → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐵) ∈ (𝐺 lim 𝐵))))
250132, 202, 249syl2anc 575 . . . . . . . . . . 11 (𝜑 → (𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺𝐵) ∈ (𝐺 lim 𝐵))))
25142, 248, 250mpbir2and 695 . . . . . . . . . 10 (𝜑𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
252251adantr 468 . . . . . . . . 9 ((𝜑𝑦 = 𝐵) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
253 fveq2 6415 . . . . . . . . . . 11 (𝑦 = 𝐵 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵))
254253eqcomd 2823 . . . . . . . . . 10 (𝑦 = 𝐵 → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
255254adantl 469 . . . . . . . . 9 ((𝜑𝑦 = 𝐵) → ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
256252, 255eleqtrd 2898 . . . . . . . 8 ((𝜑𝑦 = 𝐵) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
257200, 256jaodan 971 . . . . . . 7 ((𝜑 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
258179, 257sylan2 582 . . . . . 6 ((𝜑𝑦 ∈ {𝐴, 𝐵}) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
259178, 258jaodan 971 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
26047, 259syldan 581 . . . 4 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → 𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
261260ralrimiva 3165 . . 3 (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
262101cnfldtopon 22807 . . . . 5 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
263 resttopon 21187 . . . . 5 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴[,]𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)))
264262, 132, 263sylancr 577 . . . 4 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)))
265 cncnp 21306 . . . 4 ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
266264, 262, 265sylancl 576 . . 3 (𝜑 → (𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
26742, 261, 266mpbir2and 695 . 2 (𝜑𝐺 ∈ (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
268101, 192, 107cncfcn 22933 . . 3 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
269132, 100, 268sylancl 576 . 2 (𝜑 → ((𝐴[,]𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
270267, 269eleqtrrd 2899 1 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wnf 1863  wcel 2157  wne 2989  wral 3107  Vcvv 3402  cdif 3777  cun 3778  cin 3779  wss 3780  ifcif 4290  {cpr 4383   cuni 4641   class class class wbr 4855  cmpt 4934  ran crn 5323  cres 5324  wf 6104  cfv 6108  (class class class)co 6881  cc 10226  cr 10227  *cxr 10365   < clt 10366  cle 10367  (,)cioo 12400  [,]cicc 12403  t crest 16293  TopOpenctopn 16294  topGenctg 16310  fldccnfld 19961  Topctop 20919  TopOnctopon 20936  intcnt 21043   Cn ccn 21250   CnP ccnp 21251  cnccncf 22900   lim climc 23850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4975  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186  ax-cnex 10284  ax-resscn 10285  ax-1cn 10286  ax-icn 10287  ax-addcl 10288  ax-addrcl 10289  ax-mulcl 10290  ax-mulrcl 10291  ax-mulcom 10292  ax-addass 10293  ax-mulass 10294  ax-distr 10295  ax-i2m1 10296  ax-1ne0 10297  ax-1rid 10298  ax-rnegex 10299  ax-rrecex 10300  ax-cnre 10301  ax-pre-lttri 10302  ax-pre-lttrn 10303  ax-pre-ltadd 10304  ax-pre-mulgt0 10305  ax-pre-sup 10306
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5230  df-eprel 5235  df-po 5243  df-so 5244  df-fr 5281  df-we 5283  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-pred 5904  df-ord 5950  df-on 5951  df-lim 5952  df-suc 5953  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-riota 6842  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-om 7303  df-1st 7405  df-2nd 7406  df-wrecs 7649  df-recs 7711  df-rdg 7749  df-1o 7803  df-oadd 7807  df-er 7986  df-map 8101  df-pm 8102  df-en 8200  df-dom 8201  df-sdom 8202  df-fin 8203  df-fi 8563  df-sup 8594  df-inf 8595  df-pnf 10368  df-mnf 10369  df-xr 10370  df-ltxr 10371  df-le 10372  df-sub 10560  df-neg 10561  df-div 10977  df-nn 11313  df-2 11371  df-3 11372  df-4 11373  df-5 11374  df-6 11375  df-7 11376  df-8 11377  df-9 11378  df-n0 11567  df-z 11651  df-dec 11767  df-uz 11912  df-q 12015  df-rp 12054  df-xneg 12169  df-xadd 12170  df-xmul 12171  df-ioo 12404  df-ioc 12405  df-ico 12406  df-icc 12407  df-fz 12557  df-seq 13032  df-exp 13091  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-struct 16077  df-ndx 16078  df-slot 16079  df-base 16081  df-plusg 16173  df-mulr 16174  df-starv 16175  df-tset 16179  df-ple 16180  df-ds 16182  df-unif 16183  df-rest 16295  df-topn 16296  df-topgen 16316  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-cnfld 19962  df-top 20920  df-topon 20937  df-topsp 20959  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-cn 21253  df-cnp 21254  df-xms 22346  df-ms 22347  df-cncf 22902  df-limc 23854
This theorem is referenced by:  cncfiooicc  40592
  Copyright terms: Public domain W3C validator