Metamath Proof Explorer

Theorem cnlimc

Description: F is a continuous function iff the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Assertion cnlimc ⊢ A ⊆ ℂ → F : A ⟶cn ℂ ↔ F : A ⟶ ℂ ∧ ∀ x ∈ A F ⁡ x ∈ F lim ℂ x

Proof

Step Hyp Ref Expression
1 ssid ⊢ ℂ ⊆ ℂ
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 A = TopOpen ⁡ ℂ fld ↾ 𝑡 A
4 2 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
5 4 toponrestid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
6 2 3 5 cncfcn ⊢ A ⊆ ℂ ∧ ℂ ⊆ ℂ → A ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 A Cn TopOpen ⁡ ℂ fld
7 1 6 mpan2 ⊢ A ⊆ ℂ → A ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 A Cn TopOpen ⁡ ℂ fld
8 7 eleq2d ⊢ A ⊆ ℂ → F : A ⟶cn ℂ ↔ F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A Cn TopOpen ⁡ ℂ fld
9 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ A ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 A ∈ TopOn ⁡ A
10 4 9 mpan ⊢ A ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 A ∈ TopOn ⁡ A
11 cncnp ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 A ∈ TopOn ⁡ A ∧ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ → F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A Cn TopOpen ⁡ ℂ fld ↔ F : A ⟶ ℂ ∧ ∀ x ∈ A F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A CnP TopOpen ⁡ ℂ fld ⁡ x
12 10 4 11 sylancl ⊢ A ⊆ ℂ → F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A Cn TopOpen ⁡ ℂ fld ↔ F : A ⟶ ℂ ∧ ∀ x ∈ A F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A CnP TopOpen ⁡ ℂ fld ⁡ x
13 2 3 cnplimc ⊢ A ⊆ ℂ ∧ x ∈ A → F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A CnP TopOpen ⁡ ℂ fld ⁡ x ↔ F : A ⟶ ℂ ∧ F ⁡ x ∈ F lim ℂ x
14 13 baibd ⊢ A ⊆ ℂ ∧ x ∈ A ∧ F : A ⟶ ℂ → F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A CnP TopOpen ⁡ ℂ fld ⁡ x ↔ F ⁡ x ∈ F lim ℂ x
15 14 an32s ⊢ A ⊆ ℂ ∧ F : A ⟶ ℂ ∧ x ∈ A → F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A CnP TopOpen ⁡ ℂ fld ⁡ x ↔ F ⁡ x ∈ F lim ℂ x
16 15 ralbidva ⊢ A ⊆ ℂ ∧ F : A ⟶ ℂ → ∀ x ∈ A F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A CnP TopOpen ⁡ ℂ fld ⁡ x ↔ ∀ x ∈ A F ⁡ x ∈ F lim ℂ x
17 16 pm5.32da ⊢ A ⊆ ℂ → F : A ⟶ ℂ ∧ ∀ x ∈ A F ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 A CnP TopOpen ⁡ ℂ fld ⁡ x ↔ F : A ⟶ ℂ ∧ ∀ x ∈ A F ⁡ x ∈ F lim ℂ x
18 8 12 17 3bitrd ⊢ A ⊆ ℂ → F : A ⟶cn ℂ ↔ F : A ⟶ ℂ ∧ ∀ x ∈ A F ⁡ x ∈ F lim ℂ x