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

Metamath Proof Explorer

Theorem cnmptlimc

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	cnmptlimc.f	\|- ( ph -> ( x e. A \|-> X ) e. ( A -cn-> D ) )
		cnmptlimc.b	\|- ( ph -> B e. A )
		cnmptlimc.1	\|- ( x = B -> X = Y )
	Assertion	cnmptlimc	\|- ( ph -> Y e. ( ( x e. A \|-> X ) limCC B ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptlimc.f	\|- ( ph -> ( x e. A \|-> X ) e. ( A -cn-> D ) )
2		cnmptlimc.b	\|- ( ph -> B e. A )
3		cnmptlimc.1	\|- ( x = B -> X = Y )
4		eqid	\|- ( x e. A \|-> X ) = ( x e. A \|-> X )
5	3	eleq1d	\|- ( x = B -> ( X e. D <-> Y e. D ) )
6		cncff	\|- ( ( x e. A \|-> X ) e. ( A -cn-> D ) -> ( x e. A \|-> X ) : A --> D )
7	1 6	syl	\|- ( ph -> ( x e. A \|-> X ) : A --> D )
8	4	fmpt	\|- ( A. x e. A X e. D <-> ( x e. A \|-> X ) : A --> D )
9	7 8	sylibr	\|- ( ph -> A. x e. A X e. D )
10	5 9 2	rspcdva	\|- ( ph -> Y e. D )
11	4 3 2 10	fvmptd3	\|- ( ph -> ( ( x e. A \|-> X ) ` B ) = Y )
12	1 2	cnlimci	\|- ( ph -> ( ( x e. A \|-> X ) ` B ) e. ( ( x e. A \|-> X ) limCC B ) )
13	11 12	eqeltrrd	\|- ( ph -> Y e. ( ( x e. A \|-> X ) limCC B ) )