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	$⊢ φ \to F : A \underset{cn}{⟶} D$
		cnlimci.c	$⊢ φ \to B \in A$
	Assertion	cnlimci	$⊢ φ \to F (B) \in (F {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		cnlimci.f	$⊢ φ \to F : A \underset{cn}{⟶} D$
2		cnlimci.c	$⊢ φ \to B \in A$
3		fveq2	$⊢ x = B \to F (x) = F (B)$
4		oveq2	$⊢ x = B \to F {lim}_{ℂ} x = F {lim}_{ℂ} B$
5	3 4	eleq12d	$⊢ x = B \to (F (x) \in (F {lim}_{ℂ} x) \leftrightarrow F (B) \in (F {lim}_{ℂ} B))$
6		cncfrss	$⊢ F : A \underset{cn}{⟶} D \to A \subseteq ℂ$
7	1 6	syl	$⊢ φ \to A \subseteq ℂ$
8		cncfrss2	$⊢ F : A \underset{cn}{⟶} D \to D \subseteq ℂ$
9	1 8	syl	$⊢ φ \to D \subseteq ℂ$
10		ssid	$⊢ ℂ \subseteq ℂ$
11		cncfss	$⊢ (D \subseteq ℂ \land ℂ \subseteq ℂ) \to A \underset{cn}{⟶} D \subseteq A \underset{cn}{⟶} ℂ$
12	9 10 11	sylancl	$⊢ φ \to A \underset{cn}{⟶} D \subseteq A \underset{cn}{⟶} ℂ$
13	12 1	sseldd	$⊢ φ \to F : A \underset{cn}{⟶} ℂ$
14		cnlimc	$⊢ A \subseteq ℂ \to (F : A \underset{cn}{⟶} ℂ \leftrightarrow (F : A ⟶ ℂ \land \forall x \in A F (x) \in (F {lim}_{ℂ} x)))$
15	14	simplbda	$⊢ (A \subseteq ℂ \land F : A \underset{cn}{⟶} ℂ) \to \forall x \in A F (x) \in (F {lim}_{ℂ} x)$
16	7 13 15	syl2anc	$⊢ φ \to \forall x \in A F (x) \in (F {lim}_{ℂ} x)$
17	5 16 2	rspcdva	$⊢ φ \to F (B) \in (F {lim}_{ℂ} B)$