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 ⊢ φ → F : A ⟶cn D
cnlimci.c ⊢ φ → B ∈ A
Assertion cnlimci ⊢ φ → F ⁡ B ∈ F lim ℂ B

Proof

Step Hyp Ref Expression
1 cnlimci.f ⊢ φ → F : A ⟶cn D
2 cnlimci.c ⊢ φ → B ∈ A
3 fveq2 ⊢ x = B → F ⁡ x = F ⁡ B
4 oveq2 ⊢ x = B → F lim ℂ x = F lim ℂ B
5 3 4 eleq12d ⊢ x = B → F ⁡ x ∈ F lim ℂ x ↔ F ⁡ B ∈ F lim ℂ B
6 cncfrss ⊢ F : A ⟶cn D → A ⊆ ℂ
7 1 6 syl ⊢ φ → A ⊆ ℂ
8 cncfrss2 ⊢ F : A ⟶cn D → D ⊆ ℂ
9 1 8 syl ⊢ φ → D ⊆ ℂ
10 ssid ⊢ ℂ ⊆ ℂ
11 cncfss ⊢ D ⊆ ℂ ∧ ℂ ⊆ ℂ → A ⟶cn D ⊆ A ⟶cn ℂ
12 9 10 11 sylancl ⊢ φ → A ⟶cn D ⊆ A ⟶cn ℂ
13 12 1 sseldd ⊢ φ → F : A ⟶cn ℂ
14 cnlimc ⊢ A ⊆ ℂ → F : A ⟶cn ℂ ↔ F : A ⟶ ℂ ∧ ∀ x ∈ A F ⁡ x ∈ F lim ℂ x
15 14 simplbda ⊢ A ⊆ ℂ ∧ F : A ⟶cn ℂ → ∀ x ∈ A F ⁡ x ∈ F lim ℂ x
16 7 13 15 syl2anc ⊢ φ → ∀ x ∈ A F ⁡ x ∈ F lim ℂ x
17 5 16 2 rspcdva ⊢ φ → F ⁡ B ∈ F lim ℂ B