Metamath Proof Explorer

Theorem dvcn

Description: A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-Sep-2015)

Ref Expression
Assertion dvcn ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→F:A⟶cnℂ

Proof

Step Hyp Ref Expression
1 simpl2 ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→F:A⟶ℂ
2 eqid ⊢TopOpen⁡ℂfld↾𝑡A=TopOpen⁡ℂfld↾𝑡A
3 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
4 2 3 dvcnp2 ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧x∈dom⁡FS′→F∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
5 4 ralrimiva ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S→∀x∈dom⁡FS′F∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
6 raleq ⊢dom⁡FS′=A→∀x∈dom⁡FS′F∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x↔∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
7 6 biimpd ⊢dom⁡FS′=A→∀x∈dom⁡FS′F∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x→∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
8 5 7 mpan9 ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
9 3 cnfldtopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ
10 simpl3 ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→A⊆S
11 simpl1 ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→S⊆ℂ
12 10 11 sstrd ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→A⊆ℂ
13 resttopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ∧A⊆ℂ→TopOpen⁡ℂfld↾𝑡A∈TopOn⁡A
14 9 12 13 sylancr ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→TopOpen⁡ℂfld↾𝑡A∈TopOn⁡A
15 cncnp ⊢TopOpen⁡ℂfld↾𝑡A∈TopOn⁡A∧TopOpen⁡ℂfld∈TopOn⁡ℂ→F∈TopOpen⁡ℂfld↾𝑡ACnTopOpen⁡ℂfld↔F:A⟶ℂ∧∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
16 14 9 15 sylancl ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→F∈TopOpen⁡ℂfld↾𝑡ACnTopOpen⁡ℂfld↔F:A⟶ℂ∧∀x∈AF∈TopOpen⁡ℂfld↾𝑡ACnPTopOpen⁡ℂfld⁡x
17 1 8 16 mpbir2and ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→F∈TopOpen⁡ℂfld↾𝑡ACnTopOpen⁡ℂfld
18 ssid ⊢ℂ⊆ℂ
19 9 toponrestid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld↾𝑡ℂ
20 3 2 19 cncfcn ⊢A⊆ℂ∧ℂ⊆ℂ→A⟶cnℂ=TopOpen⁡ℂfld↾𝑡ACnTopOpen⁡ℂfld
21 12 18 20 sylancl ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→A⟶cnℂ=TopOpen⁡ℂfld↾𝑡ACnTopOpen⁡ℂfld
22 17 21 eleqtrrd ⊢S⊆ℂ∧F:A⟶ℂ∧A⊆S∧dom⁡FS′=A→F:A⟶cnℂ