This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvbsss

Description: The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Assertion dvbsss dom ( 𝑆 D 𝐹 ) ⊆ 𝑆

Proof

Step Hyp Ref Expression
1 df-dv ⊢ D = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
2 1 reldmmpo ⊢ Rel dom D
3 df-rel ⊢ ( Rel dom D ↔ dom D ⊆ ( V × V ) )
4 2 3 mpbi ⊢ dom D ⊆ ( V × V )
5 4 sseli ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ⟨ 𝑆 , 𝐹 ⟩ ∈ ( V × V ) )
6 opelxp1 ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ ( V × V ) → 𝑆 ∈ V )
7 5 6 syl ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → 𝑆 ∈ V )
8 opeq1 ⊢ ( 𝑠 = 𝑆 → ⟨ 𝑠 , 𝐹 ⟩ = ⟨ 𝑆 , 𝐹 ⟩ )
9 8 eleq1d ⊢ ( 𝑠 = 𝑆 → ( ⟨ 𝑠 , 𝐹 ⟩ ∈ dom D ↔ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ) )
10 eleq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ 𝒫 ℂ ↔ 𝑆 ∈ 𝒫 ℂ ) )
11 oveq2 ⊢ ( 𝑠 = 𝑆 → ( ℂ ↑pm 𝑠 ) = ( ℂ ↑pm 𝑆 ) )
12 11 eleq2d ⊢ ( 𝑠 = 𝑆 → ( 𝐹 ∈ ( ℂ ↑pm 𝑠 ) ↔ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) )
13 10 12 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑠 ) ) ↔ ( 𝑆 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ) )
14 9 13 imbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ⟨ 𝑠 , 𝐹 ⟩ ∈ dom D → ( 𝑠 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑠 ) ) ) ↔ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝑆 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ) ) )
15 1 dmmpossx ⊢ dom D ⊆ ∪ 𝑠 ∈ 𝒫 ℂ ( { 𝑠 } × ( ℂ ↑pm 𝑠 ) )
16 15 sseli ⊢ ( ⟨ 𝑠 , 𝐹 ⟩ ∈ dom D → ⟨ 𝑠 , 𝐹 ⟩ ∈ ∪ 𝑠 ∈ 𝒫 ℂ ( { 𝑠 } × ( ℂ ↑pm 𝑠 ) ) )
17 opeliunxp ⊢ ( ⟨ 𝑠 , 𝐹 ⟩ ∈ ∪ 𝑠 ∈ 𝒫 ℂ ( { 𝑠 } × ( ℂ ↑pm 𝑠 ) ) ↔ ( 𝑠 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑠 ) ) )
18 16 17 sylib ⊢ ( ⟨ 𝑠 , 𝐹 ⟩ ∈ dom D → ( 𝑠 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑠 ) ) )
19 14 18 vtoclg ⊢ ( 𝑆 ∈ V → ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝑆 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ) )
20 7 19 mpcom ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝑆 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) )
21 20 simpld ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → 𝑆 ∈ 𝒫 ℂ )
22 21 elpwid ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → 𝑆 ⊆ ℂ )
23 20 simprd ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
24 cnex ⊢ ℂ ∈ V
25 elpm2g ⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ 𝒫 ℂ ) → ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
26 24 21 25 sylancr ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
27 23 26 mpbid ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) )
28 27 simpld ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → 𝐹 : dom 𝐹 ⟶ ℂ )
29 27 simprd ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom 𝐹 ⊆ 𝑆 )
30 22 28 29 dvbss ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom ( 𝑆 D 𝐹 ) ⊆ dom 𝐹 )
31 30 29 sstrd ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom ( 𝑆 D 𝐹 ) ⊆ 𝑆 )
32 df-ov ⊢ ( 𝑆 D 𝐹 ) = ( D ‘ ⟨ 𝑆 , 𝐹 ⟩ )
33 ndmfv ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( D ‘ ⟨ 𝑆 , 𝐹 ⟩ ) = ∅ )
34 32 33 eqtrid ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝑆 D 𝐹 ) = ∅ )
35 34 dmeqd ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom ( 𝑆 D 𝐹 ) = dom ∅ )
36 dm0 ⊢ dom ∅ = ∅
37 35 36 eqtrdi ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom ( 𝑆 D 𝐹 ) = ∅ )
38 0ss ⊢ ∅ ⊆ 𝑆
39 37 38 eqsstrdi ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom ( 𝑆 D 𝐹 ) ⊆ 𝑆 )
40 31 39 pm2.61i ⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆