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 F S S

Proof

Step Hyp Ref Expression
1 df-dv D = s 𝒫 , f 𝑝𝑚 s x int TopOpen fld 𝑡 s dom f x × z dom f x f z f x z x lim x
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 S F dom D S F V × V
6 opelxp1 S F V × V S V
7 5 6 syl S F dom D S V
8 opeq1 s = S s F = S F
9 8 eleq1d s = S s F dom D S F dom D
10 eleq1 s = S s 𝒫 S 𝒫
11 oveq2 s = S 𝑝𝑚 s = 𝑝𝑚 S
12 11 eleq2d s = S F 𝑝𝑚 s F 𝑝𝑚 S
13 10 12 anbi12d s = S s 𝒫 F 𝑝𝑚 s S 𝒫 F 𝑝𝑚 S
14 9 13 imbi12d s = S s F dom D s 𝒫 F 𝑝𝑚 s S F dom D S 𝒫 F 𝑝𝑚 S
15 1 dmmpossx dom D s 𝒫 s × 𝑝𝑚 s
16 15 sseli s F dom D s F s 𝒫 s × 𝑝𝑚 s
17 opeliunxp s F s 𝒫 s × 𝑝𝑚 s s 𝒫 F 𝑝𝑚 s
18 16 17 sylib s F dom D s 𝒫 F 𝑝𝑚 s
19 14 18 vtoclg S V S F dom D S 𝒫 F 𝑝𝑚 S
20 7 19 mpcom S F dom D S 𝒫 F 𝑝𝑚 S
21 20 simpld S F dom D S 𝒫
22 21 elpwid S F dom D S
23 20 simprd S F dom D F 𝑝𝑚 S
24 cnex V
25 elpm2g V S 𝒫 F 𝑝𝑚 S F : dom F dom F S
26 24 21 25 sylancr S F dom D F 𝑝𝑚 S F : dom F dom F S
27 23 26 mpbid S F dom D F : dom F dom F S
28 27 simpld S F dom D F : dom F
29 27 simprd S F dom D dom F S
30 22 28 29 dvbss S F dom D dom F S dom F
31 30 29 sstrd S F dom D dom F S S
32 df-ov S D F = D S F
33 ndmfv ¬ S F dom D D S F =
34 32 33 syl5eq ¬ S F dom D S D F =
35 34 dmeqd ¬ S F dom D dom F S = dom
36 dm0 dom =
37 35 36 syl6eq ¬ S F dom D dom F S =
38 0ss S
39 37 38 eqsstrdi ¬ S F dom D dom F S S
40 31 39 pm2.61i dom F S S