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 eqtr3id φ = 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