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 
|- ( ph -> A e. RR* )
ioccncflimc.b 
|- ( ph -> B e. RR )
ioccncflimc.altb 
|- ( ph -> A < B )
ioccncflimc.f 
|- ( ph -> F e. ( ( A (,] B ) -cn-> CC ) )
Assertion ioccncflimc 
|- ( ph -> ( F ` B ) e. ( ( F |` ( A (,) B ) ) limCC B ) )

Proof

Step Hyp Ref Expression
1 ioccncflimc.a 
 |-  ( ph -> A e. RR* )
2 ioccncflimc.b 
 |-  ( ph -> B e. RR )
3 ioccncflimc.altb 
 |-  ( ph -> A < B )
4 ioccncflimc.f 
 |-  ( ph -> F e. ( ( A (,] B ) -cn-> CC ) )
5 2 rexrd 
 |-  ( ph -> B e. RR* )
6 2 leidd 
 |-  ( ph -> B <_ B )
7 1 5 5 3 6 eliocd 
 |-  ( ph -> B e. ( A (,] B ) )
8 4 7 cnlimci 
 |-  ( ph -> ( F ` B ) e. ( F limCC B ) )
9 cncfrss 
 |-  ( F e. ( ( A (,] B ) -cn-> CC ) -> ( A (,] B ) C_ CC )
10 4 9 syl 
 |-  ( ph -> ( A (,] B ) C_ CC )
11 ssid 
 |-  CC C_ CC
12 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
13 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,] B ) )
14 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( ( TopOpen ` CCfld ) |`t CC )
15 12 13 14 cncfcn 
 |-  ( ( ( A (,] B ) C_ CC /\ CC C_ CC ) -> ( ( A (,] B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) )
16 10 11 15 sylancl 
 |-  ( ph -> ( ( A (,] B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) )
17 4 16 eleqtrd 
 |-  ( ph -> F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) )
18 12 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
19 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( A (,] B ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) e. ( TopOn ` ( A (,] B ) ) )
20 18 10 19 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) e. ( TopOn ` ( A (,] B ) ) )
21 12 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
22 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
23 22 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
24 21 23 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
25 24 cnfldtopon 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) e. ( TopOn ` CC )
26 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) e. ( TopOn ` ( A (,] B ) ) /\ ( ( TopOpen ` CCfld ) |`t CC ) e. ( TopOn ` CC ) ) -> ( F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) <-> ( F : ( A (,] B ) --> CC /\ A. x e. ( A (,] B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) CnP ( ( TopOpen ` CCfld ) |`t CC ) ) ` x ) ) ) )
27 20 25 26 sylancl 
 |-  ( ph -> ( F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) <-> ( F : ( A (,] B ) --> CC /\ A. x e. ( A (,] B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) CnP ( ( TopOpen ` CCfld ) |`t CC ) ) ` x ) ) ) )
28 17 27 mpbid 
 |-  ( ph -> ( F : ( A (,] B ) --> CC /\ A. x e. ( A (,] B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) CnP ( ( TopOpen ` CCfld ) |`t CC ) ) ` x ) ) )
29 28 simpld 
 |-  ( ph -> F : ( A (,] B ) --> CC )
30 ioossioc 
 |-  ( A (,) B ) C_ ( A (,] B )
31 30 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A (,] B ) )
32 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( A (,] B ) u. { B } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A (,] B ) u. { B } ) )
33 2 recnd 
 |-  ( ph -> B e. CC )
34 22 ntrtop 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) = CC )
35 21 34 ax-mp 
 |-  ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) = CC
36 undif 
 |-  ( ( A (,] B ) C_ CC <-> ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) = CC )
37 10 36 sylib 
 |-  ( ph -> ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) = CC )
38 37 eqcomd 
 |-  ( ph -> CC = ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) )
39 38 fveq2d 
 |-  ( ph -> ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) = ( ( int ` ( TopOpen ` CCfld ) ) ` ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) ) )
40 35 39 eqtr3id 
 |-  ( ph -> CC = ( ( int ` ( TopOpen ` CCfld ) ) ` ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) ) )
41 33 40 eleqtrd 
 |-  ( ph -> B e. ( ( int ` ( TopOpen ` CCfld ) ) ` ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) ) )
42 41 7 elind 
 |-  ( ph -> B e. ( ( ( int ` ( TopOpen ` CCfld ) ) ` ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) ) i^i ( A (,] B ) ) )
43 21 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
44 ssid 
 |-  ( A (,] B ) C_ ( A (,] B )
45 44 a1i 
 |-  ( ph -> ( A (,] B ) C_ ( A (,] B ) )
46 22 13 restntr 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( A (,] B ) C_ CC /\ ( A (,] B ) C_ ( A (,] B ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) ) ` ( A (,] B ) ) = ( ( ( int ` ( TopOpen ` CCfld ) ) ` ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) ) i^i ( A (,] B ) ) )
47 43 10 45 46 syl3anc 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) ) ` ( A (,] B ) ) = ( ( ( int ` ( TopOpen ` CCfld ) ) ` ( ( A (,] B ) u. ( CC \ ( A (,] B ) ) ) ) i^i ( A (,] B ) ) )
48 42 47 eleqtrrd 
 |-  ( ph -> B e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) ) ` ( A (,] B ) ) )
49 7 snssd 
 |-  ( ph -> { B } C_ ( A (,] B ) )
50 ssequn2 
 |-  ( { B } C_ ( A (,] B ) <-> ( ( A (,] B ) u. { B } ) = ( A (,] B ) )
51 49 50 sylib 
 |-  ( ph -> ( ( A (,] B ) u. { B } ) = ( A (,] B ) )
52 51 eqcomd 
 |-  ( ph -> ( A (,] B ) = ( ( A (,] B ) u. { B } ) )
53 52 oveq2d 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A (,] B ) u. { B } ) ) )
54 53 fveq2d 
 |-  ( ph -> ( int ` ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A (,] B ) u. { B } ) ) ) )
55 ioounsn 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
56 1 5 3 55 syl3anc 
 |-  ( ph -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
57 56 eqcomd 
 |-  ( ph -> ( A (,] B ) = ( ( A (,) B ) u. { B } ) )
58 54 57 fveq12d 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) ) ` ( A (,] B ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A (,] B ) u. { B } ) ) ) ` ( ( A (,) B ) u. { B } ) ) )
59 48 58 eleqtrd 
 |-  ( ph -> B e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A (,] B ) u. { B } ) ) ) ` ( ( A (,) B ) u. { B } ) ) )
60 29 31 10 12 32 59 limcres 
 |-  ( ph -> ( ( F |` ( A (,) B ) ) limCC B ) = ( F limCC B ) )
61 8 60 eleqtrrd 
 |-  ( ph -> ( F ` B ) e. ( ( F |` ( A (,) B ) ) limCC B ) )