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 ) )