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

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 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –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ℂ 𝐵 ) )