Metamath Proof Explorer

Theorem icocncflimc

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

Ref Expression
Hypotheses icocncflimc.a 
|- ( ph -> A e. RR )
icocncflimc.b 
|- ( ph -> B e. RR* )
icocncflimc.altb 
|- ( ph -> A < B )
icocncflimc.f 
|- ( ph -> F e. ( ( A [,) B ) -cn-> CC ) )
Assertion icocncflimc 
|- ( ph -> ( F ` A ) e. ( ( F |` ( A (,) B ) ) limCC A ) )

Proof

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