Metamath Proof Explorer

Theorem ioccncflimc

Description: Limit at the upper bound of a continuous function defined on a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ioccncflimc.a ⊢ φ → A ∈ ℝ *
ioccncflimc.b ⊢ φ → B ∈ ℝ
ioccncflimc.altb ⊢ φ → A < B
ioccncflimc.f ⊢ φ → F : A B ⟶cn ℂ
Assertion ioccncflimc ⊢ φ → F ⁡ B ∈ F ↾ A B lim ℂ B

Proof

Step Hyp Ref Expression
1 ioccncflimc.a ⊢ φ → A ∈ ℝ *
2 ioccncflimc.b ⊢ φ → B ∈ ℝ
3 ioccncflimc.altb ⊢ φ → A < B
4 ioccncflimc.f ⊢ φ → F : A B ⟶cn ℂ
5 2 rexrd ⊢ φ → B ∈ ℝ *
6 2 leidd ⊢ φ → B ≤ B
7 1 5 5 3 6 eliocd ⊢ φ → B ∈ A B
8 4 7 cnlimci ⊢ φ → F ⁡ B ∈ F lim ℂ B
9 cncfrss ⊢ F : A B ⟶cn ℂ → A B ⊆ ℂ
10 4 9 syl ⊢ φ → A B ⊆ ℂ
11 ssid ⊢ ℂ ⊆ ℂ
12 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
13 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 A B = TopOpen ⁡ ℂ fld ↾ 𝑡 A B
14 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
15 12 13 14 cncfcn ⊢ A B ⊆ ℂ ∧ ℂ ⊆ ℂ → A B ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 A B Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
16 10 11 15 sylancl ⊢ φ → A B ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 A B Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
17 4 16 eleqtrd ⊢ φ → F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A B Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
18 12 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
19 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ A B ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∈ TopOn ⁡ A B
20 18 10 19 sylancr ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∈ TopOn ⁡ A B
21 12 cnfldtop ⊢ TopOpen ⁡ ℂ fld ∈ Top
22 unicntop ⊢ ℂ = ⋃ TopOpen ⁡ ℂ fld
23 22 restid ⊢ TopOpen ⁡ ℂ fld ∈ Top → TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ = TopOpen ⁡ ℂ fld
24 21 23 ax-mp ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ = TopOpen ⁡ ℂ fld
25 24 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ ∈ TopOn ⁡ ℂ
26 cncnp ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∈ TopOn ⁡ A B ∧ TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ ∈ TopOn ⁡ ℂ → F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A B Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ ↔ F : A B ⟶ ℂ ∧ ∀ x ∈ A B F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A B CnP TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ ⁡ x
27 20 25 26 sylancl ⊢ φ → F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A B Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ ↔ F : A B ⟶ ℂ ∧ ∀ x ∈ A B F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A B CnP TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ ⁡ x
28 17 27 mpbid ⊢ φ → F : A B ⟶ ℂ ∧ ∀ x ∈ A B F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A B CnP TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ ⁡ x
29 28 simpld ⊢ φ → F : A B ⟶ ℂ
30 ioossioc ⊢ A B ⊆ A B
31 30 a1i ⊢ φ → A B ⊆ A B
32 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∪ B = TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∪ B
33 2 recnd ⊢ φ → B ∈ ℂ
34 22 ntrtop ⊢ TopOpen ⁡ ℂ fld ∈ Top → int ⁡ TopOpen ⁡ ℂ fld ⁡ ℂ = ℂ
35 21 34 ax-mp ⊢ int ⁡ TopOpen ⁡ ℂ fld ⁡ ℂ = ℂ
36 undif ⊢ A B ⊆ ℂ ↔ A B ∪ ℂ ∖ A B = ℂ
37 10 36 sylib ⊢ φ → A B ∪ ℂ ∖ A B = ℂ
38 37 eqcomd ⊢ φ → ℂ = A B ∪ ℂ ∖ A B
39 38 fveq2d ⊢ φ → int ⁡ TopOpen ⁡ ℂ fld ⁡ ℂ = int ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∪ ℂ ∖ A B
40 35 39 syl5eqr ⊢ φ → ℂ = int ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∪ ℂ ∖ A B
41 33 40 eleqtrd ⊢ φ → B ∈ int ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∪ ℂ ∖ A B
42 41 7 elind ⊢ φ → B ∈ int ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∪ ℂ ∖ A B ∩ A B
43 21 a1i ⊢ φ → TopOpen ⁡ ℂ fld ∈ Top
44 ssid ⊢ A B ⊆ A B
45 44 a1i ⊢ φ → A B ⊆ A B
46 22 13 restntr ⊢ TopOpen ⁡ ℂ fld ∈ Top ∧ A B ⊆ ℂ ∧ A B ⊆ A B → int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ⁡ A B = int ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∪ ℂ ∖ A B ∩ A B
47 43 10 45 46 syl3anc ⊢ φ → int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ⁡ A B = int ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∪ ℂ ∖ A B ∩ A B
48 42 47 eleqtrrd ⊢ φ → B ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ⁡ A B
49 7 snssd ⊢ φ → B ⊆ A B
50 ssequn2 ⊢ B ⊆ A B ↔ A B ∪ B = A B
51 49 50 sylib ⊢ φ → A B ∪ B = A B
52 51 eqcomd ⊢ φ → A B = A B ∪ B
53 52 oveq2d ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 A B = TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∪ B
54 53 fveq2d ⊢ φ → int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 A B = int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∪ B
55 ioounsn ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A < B → A B ∪ B = A B
56 1 5 3 55 syl3anc ⊢ φ → A B ∪ B = A B
57 56 eqcomd ⊢ φ → A B = A B ∪ B
58 54 57 fveq12d ⊢ φ → int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ⁡ A B = int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∪ B ⁡ A B ∪ B
59 48 58 eleqtrd ⊢ φ → B ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 A B ∪ B ⁡ A B ∪ B
60 29 31 10 12 32 59 limcres ⊢ φ → F ↾ A B lim ℂ B = F lim ℂ B
61 8 60 eleqtrrd ⊢ φ → F ⁡ B ∈ F ↾ A B lim ℂ B