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	$⊢ φ \to (x \in A ⟼ X) : A \underset{cn}{⟶} D$
		cnmptlimc.b	$⊢ φ \to B \in A$
		cnmptlimc.1	$⊢ x = B \to X = Y$
	Assertion	cnmptlimc	$⊢ φ \to Y \in ((x \in A ⟼ X) {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		cnmptlimc.f	$⊢ φ \to (x \in A ⟼ X) : A \underset{cn}{⟶} D$
2		cnmptlimc.b	$⊢ φ \to B \in A$
3		cnmptlimc.1	$⊢ x = B \to X = Y$
4		eqid	$⊢ (x \in A ⟼ X) = (x \in A ⟼ X)$
5	3	eleq1d	$⊢ x = B \to (X \in D \leftrightarrow Y \in D)$
6		cncff	$⊢ (x \in A ⟼ X) : A \underset{cn}{⟶} D \to (x \in A ⟼ X) : A ⟶ D$
7	1 6	syl	$⊢ φ \to (x \in A ⟼ X) : A ⟶ D$
8	4	fmpt	$⊢ \forall x \in A X \in D \leftrightarrow (x \in A ⟼ X) : A ⟶ D$
9	7 8	sylibr	$⊢ φ \to \forall x \in A X \in D$
10	5 9 2	rspcdva	$⊢ φ \to Y \in D$
11	4 3 2 10	fvmptd3	$⊢ φ \to (x \in A ⟼ X) (B) = Y$
12	1 2	cnlimci	$⊢ φ \to (x \in A ⟼ X) (B) \in ((x \in A ⟼ X) {lim}_{ℂ} B)$
13	11 12	eqeltrrd	$⊢ φ \to Y \in ((x \in A ⟼ X) {lim}_{ℂ} B)$