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	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) ∈ ( 𝐴 –cn→ 𝐷 ) )
		cnmptlimc.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
		cnmptlimc.1	⊢ ( 𝑥 = 𝐵 → 𝑋 = 𝑌 )
	Assertion	cnmptlimc	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) lim_ℂ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptlimc.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) ∈ ( 𝐴 –cn→ 𝐷 ) )
2		cnmptlimc.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		cnmptlimc.1	⊢ ( 𝑥 = 𝐵 → 𝑋 = 𝑌 )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑋 )
5	3	eleq1d	⊢ ( 𝑥 = 𝐵 → ( 𝑋 ∈ 𝐷 ↔ 𝑌 ∈ 𝐷 ) )
6		cncff	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) ∈ ( 𝐴 –cn→ 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ 𝐷 )
7	1 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ 𝐷 )
8	4	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐷 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ 𝐷 )
9	7 8	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐷 )
10	5 9 2	rspcdva	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11	4 3 2 10	fvmptd3	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) ‘ 𝐵 ) = 𝑌 )
12	1 2	cnlimci	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) ‘ 𝐵 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) lim_ℂ 𝐵 ) )
13	11 12	eqeltrrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) lim_ℂ 𝐵 ) )