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 ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → 𝐹 : 𝐴 ⟶ ℂ )
2 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 )
3 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4 2 3 dvcnp2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝑥 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
5 4 ralrimiva ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ∀ 𝑥 ∈ dom ( 𝑆 D 𝐹 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
6 raleq ⊢ ( dom ( 𝑆 D 𝐹 ) = 𝐴 → ( ∀ 𝑥 ∈ dom ( 𝑆 D 𝐹 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
7 6 biimpd ⊢ ( dom ( 𝑆 D 𝐹 ) = 𝐴 → ( ∀ 𝑥 ∈ dom ( 𝑆 D 𝐹 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
8 5 7 mpan9 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
9 3 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
10 simpl3 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → 𝐴 ⊆ 𝑆 )
11 simpl1 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → 𝑆 ⊆ ℂ )
12 10 11 sstrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → 𝐴 ⊆ ℂ )
13 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
14 9 12 13 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
15 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
16 14 9 15 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
17 1 8 16 mpbir2and ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
18 ssid ⊢ ℂ ⊆ ℂ
19 9 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
20 3 2 19 cncfcn ⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐴 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
21 12 18 20 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → ( 𝐴 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
22 17 21 eleqtrrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝐴 ) → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )