This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnlimci

Description: If F is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses cnlimci.f 
|- ( ph -> F e. ( A -cn-> D ) )
cnlimci.c 
|- ( ph -> B e. A )
Assertion cnlimci 
|- ( ph -> ( F ` B ) e. ( F limCC B ) )

Proof

Step Hyp Ref Expression
1 cnlimci.f 
 |-  ( ph -> F e. ( A -cn-> D ) )
2 cnlimci.c 
 |-  ( ph -> B e. A )
3 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
4 oveq2 
 |-  ( x = B -> ( F limCC x ) = ( F limCC B ) )
5 3 4 eleq12d 
 |-  ( x = B -> ( ( F ` x ) e. ( F limCC x ) <-> ( F ` B ) e. ( F limCC B ) ) )
6 cncfrss 
 |-  ( F e. ( A -cn-> D ) -> A C_ CC )
7 1 6 syl 
 |-  ( ph -> A C_ CC )
8 cncfrss2 
 |-  ( F e. ( A -cn-> D ) -> D C_ CC )
9 1 8 syl 
 |-  ( ph -> D C_ CC )
10 ssid 
 |-  CC C_ CC
11 cncfss 
 |-  ( ( D C_ CC /\ CC C_ CC ) -> ( A -cn-> D ) C_ ( A -cn-> CC ) )
12 9 10 11 sylancl 
 |-  ( ph -> ( A -cn-> D ) C_ ( A -cn-> CC ) )
13 12 1 sseldd 
 |-  ( ph -> F e. ( A -cn-> CC ) )
14 cnlimc 
 |-  ( A C_ CC -> ( F e. ( A -cn-> CC ) <-> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F limCC x ) ) ) )
15 14 simplbda 
 |-  ( ( A C_ CC /\ F e. ( A -cn-> CC ) ) -> A. x e. A ( F ` x ) e. ( F limCC x ) )
16 7 13 15 syl2anc 
 |-  ( ph -> A. x e. A ( F ` x ) e. ( F limCC x ) )
17 5 16 2 rspcdva 
 |-  ( ph -> ( F ` B ) e. ( F limCC B ) )