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∈AF⁡x∈Flimℂ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↾𝑡ACnTopOpen⁡ℂfld
7 1 6 mpan2 ⊢A⊆ℂ→A⟶cnℂ=TopOpen⁡ℂfld↾𝑡ACnTopOpen⁡ℂfld
8 7 eleq2d ⊢A⊆ℂ→F:A⟶cnℂ↔F∈TopOpen⁡ℂfld↾𝑡ACnTopOpen⁡ℂ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↾𝑡ACnTopOpen⁡ℂfld↔F:A⟶ℂ∧∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
12 10 4 11 sylancl ⊢A⊆ℂ→F∈TopOpen⁡ℂfld↾𝑡ACnTopOpen⁡ℂfld↔F:A⟶ℂ∧∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
13 2 3 cnplimc ⊢A⊆ℂ∧x∈A→F∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x↔F:A⟶ℂ∧F⁡x∈Flimℂx
14 13 baibd ⊢A⊆ℂ∧x∈A∧F:A⟶ℂ→F∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x↔F⁡x∈Flimℂx
15 14 an32s ⊢A⊆ℂ∧F:A⟶ℂ∧x∈A→F∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x↔F⁡x∈Flimℂx
16 15 ralbidva ⊢A⊆ℂ∧F:A⟶ℂ→∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x↔∀x∈AF⁡x∈Flimℂx
17 16 pm5.32da ⊢A⊆ℂ→F:A⟶ℂ∧∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x↔F:A⟶ℂ∧∀x∈AF⁡x∈Flimℂx
18 8 12 17 3bitrd ⊢A⊆ℂ→F:A⟶cnℂ↔F:A⟶ℂ∧∀x∈AF⁡x∈Flimℂx