Metamath Proof Explorer

Theorem dvfval

Description: Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses dvval.t ⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
dvval.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion dvfval ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( ( 𝑆 D 𝐹 ) = ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ∧ ( 𝑆 D 𝐹 ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ ) ) )

Proof

Step Hyp Ref Expression
1 dvval.t ⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
2 dvval.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3 df-dv ⊢ D = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
4 3 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → D = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ) )
5 2 oveq1i ⊢ ( 𝐾 ↾t 𝑠 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 )
6 simprl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → 𝑠 = 𝑆 )
7 6 oveq2d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝐾 ↾t 𝑠 ) = ( 𝐾 ↾t 𝑆 ) )
8 7 1 eqtr4di ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝐾 ↾t 𝑠 ) = 𝑇 )
9 5 8 eqtr3id ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) = 𝑇 )
10 9 fveq2d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) = ( int ‘ 𝑇 ) )
11 simprr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
12 11 dmeqd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → dom 𝑓 = dom 𝐹 )
13 simpl2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
14 13 fdmd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → dom 𝐹 = 𝐴 )
15 12 14 eqtrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → dom 𝑓 = 𝐴 )
16 10 15 fveq12d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) = ( ( int ‘ 𝑇 ) ‘ 𝐴 ) )
17 15 difeq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( dom 𝑓 ∖ { 𝑥 } ) = ( 𝐴 ∖ { 𝑥 } ) )
18 11 fveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
19 11 fveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
20 18 19 oveq12d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) )
21 20 oveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
22 17 21 mpteq12dv ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) )
23 22 oveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
24 23 xpeq2d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) = ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
25 16 24 iuneq12d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) = ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
26 simpr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
27 26 oveq2d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝑠 = 𝑆 ) → ( ℂ ↑pm 𝑠 ) = ( ℂ ↑pm 𝑆 ) )
28 simp1 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝑆 ⊆ ℂ )
29 cnex ⊢ ℂ ∈ V
30 29 elpw2 ⊢ ( 𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ )
31 28 30 sylibr ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝑆 ∈ 𝒫 ℂ )
32 29 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ℂ ∈ V )
33 simp2 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐹 : 𝐴 ⟶ ℂ )
34 simp3 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐴 ⊆ 𝑆 )
35 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ 𝒫 ℂ ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
36 32 31 33 34 35 syl22anc ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
37 limccl ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ⊆ ℂ
38 xpss2 ⊢ ( ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ⊆ ℂ → ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( { 𝑥 } × ℂ ) )
39 37 38 ax-mp ⊢ ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( { 𝑥 } × ℂ )
40 39 rgenw ⊢ ∀ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( { 𝑥 } × ℂ )
41 ss2iun ⊢ ( ∀ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( { 𝑥 } × ℂ ) → ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ℂ ) )
42 40 41 ax-mp ⊢ ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ℂ )
43 iunxpconst ⊢ ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ℂ ) = ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ )
44 42 43 sseqtri ⊢ ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ )
45 44 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ ) )
46 fvex ⊢ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∈ V
47 46 29 xpex ⊢ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ ) ∈ V
48 47 ssex ⊢ ( ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ ) → ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ∈ V )
49 45 48 syl ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ∈ V )
50 4 25 27 31 36 49 ovmpodx ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝑆 D 𝐹 ) = ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
51 50 45 eqsstrd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝑆 D 𝐹 ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ ) )
52 50 51 jca ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( ( 𝑆 D 𝐹 ) = ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ∧ ( 𝑆 D 𝐹 ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ ) ) )