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	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐷 ) )
	cnlimci.c	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
Assertion	cnlimci	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cnlimci.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐷 ) )
2		cnlimci.c	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		fveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
4		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐹 limℂ 𝑥 ) = ( 𝐹 limℂ 𝐵 ) )
5	3 4	eleq12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) )
6		cncfrss	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐷 ) → 𝐴 ⊆ ℂ )
7	1 6	syl	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
8		cncfrss2	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐷 ) → 𝐷 ⊆ ℂ )
9	1 8	syl	⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
10		ssid	⊢ ℂ ⊆ ℂ
11		cncfss	⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐴 –cn→ 𝐷 ) ⊆ ( 𝐴 –cn→ ℂ ) )
12	9 10 11	sylancl	⊢ ( 𝜑 → ( 𝐴 –cn→ 𝐷 ) ⊆ ( 𝐴 –cn→ ℂ ) )
13	12 1	sseldd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
14		cnlimc	⊢ ( 𝐴 ⊆ ℂ → ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ) ) )
15	14	simplbda	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) )
16	7 13 15	syl2anc	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) )
17	5 16 2	rspcdva	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) )