Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dvbss | Structured version Visualization version GIF version |
Description: The set of differentiable points is a subset of the domain of the function. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
Ref | Expression |
---|---|
dvcl.s | ⊢ (𝜑 → 𝑆 ⊆ ℂ) |
dvcl.f | ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
dvcl.a | ⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
Ref | Expression |
---|---|
dvbss | ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvcl.s | . . 3 ⊢ (𝜑 → 𝑆 ⊆ ℂ) | |
2 | dvcl.f | . . 3 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | |
3 | dvcl.a | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝑆) | |
4 | eqid 2738 | . . 3 ⊢ ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆) | |
5 | eqid 2738 | . . 3 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld) | |
6 | 1, 2, 3, 4, 5 | dvbssntr 25052 | . 2 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴)) |
7 | 5 | cnfldtop 23935 | . . . 4 ⊢ (TopOpen‘ℂfld) ∈ Top |
8 | cnex 10940 | . . . . 5 ⊢ ℂ ∈ V | |
9 | ssexg 5246 | . . . . 5 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V) | |
10 | 1, 8, 9 | sylancl 586 | . . . 4 ⊢ (𝜑 → 𝑆 ∈ V) |
11 | resttop 22299 | . . . 4 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) | |
12 | 7, 10, 11 | sylancr 587 | . . 3 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
13 | 5 | cnfldtopon 23934 | . . . . . 6 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ) |
14 | resttopon 22300 | . . . . . 6 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) | |
15 | 13, 1, 14 | sylancr 587 | . . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
16 | toponuni 22051 | . . . . 5 ⊢ (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ ((TopOpen‘ℂfld) ↾t 𝑆)) | |
17 | 15, 16 | syl 17 | . . . 4 ⊢ (𝜑 → 𝑆 = ∪ ((TopOpen‘ℂfld) ↾t 𝑆)) |
18 | 3, 17 | sseqtrd 3961 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ ∪ ((TopOpen‘ℂfld) ↾t 𝑆)) |
19 | eqid 2738 | . . . 4 ⊢ ∪ ((TopOpen‘ℂfld) ↾t 𝑆) = ∪ ((TopOpen‘ℂfld) ↾t 𝑆) | |
20 | 19 | ntrss2 22196 | . . 3 ⊢ ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ ((TopOpen‘ℂfld) ↾t 𝑆)) → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴) |
21 | 12, 18, 20 | syl2anc 584 | . 2 ⊢ (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴) |
22 | 6, 21 | sstrd 3931 | 1 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2106 Vcvv 3430 ⊆ wss 3887 ∪ cuni 4840 dom cdm 5585 ⟶wf 6423 ‘cfv 6427 (class class class)co 7268 ℂcc 10857 ↾t crest 17119 TopOpenctopn 17120 ℂfldccnfld 20585 Topctop 22030 TopOnctopon 22047 intcnt 22156 D cdv 25015 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5222 ax-nul 5229 ax-pow 5287 ax-pr 5351 ax-un 7579 ax-cnex 10915 ax-resscn 10916 ax-1cn 10917 ax-icn 10918 ax-addcl 10919 ax-addrcl 10920 ax-mulcl 10921 ax-mulrcl 10922 ax-mulcom 10923 ax-addass 10924 ax-mulass 10925 ax-distr 10926 ax-i2m1 10927 ax-1ne0 10928 ax-1rid 10929 ax-rnegex 10930 ax-rrecex 10931 ax-cnre 10932 ax-pre-lttri 10933 ax-pre-lttrn 10934 ax-pre-ltadd 10935 ax-pre-mulgt0 10936 ax-pre-sup 10937 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3432 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5485 df-eprel 5491 df-po 5499 df-so 5500 df-fr 5540 df-we 5542 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-pred 6196 df-ord 6263 df-on 6264 df-lim 6265 df-suc 6266 df-iota 6385 df-fun 6429 df-fn 6430 df-f 6431 df-f1 6432 df-fo 6433 df-f1o 6434 df-fv 6435 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-om 7704 df-1st 7821 df-2nd 7822 df-frecs 8085 df-wrecs 8116 df-recs 8190 df-rdg 8229 df-1o 8285 df-er 8486 df-map 8605 df-pm 8606 df-en 8722 df-dom 8723 df-sdom 8724 df-fin 8725 df-fi 9158 df-sup 9189 df-inf 9190 df-pnf 10999 df-mnf 11000 df-xr 11001 df-ltxr 11002 df-le 11003 df-sub 11195 df-neg 11196 df-div 11621 df-nn 11962 df-2 12024 df-3 12025 df-4 12026 df-5 12027 df-6 12028 df-7 12029 df-8 12030 df-9 12031 df-n0 12222 df-z 12308 df-dec 12426 df-uz 12571 df-q 12677 df-rp 12719 df-xneg 12836 df-xadd 12837 df-xmul 12838 df-fz 13228 df-seq 13710 df-exp 13771 df-cj 14798 df-re 14799 df-im 14800 df-sqrt 14934 df-abs 14935 df-struct 16836 df-slot 16871 df-ndx 16883 df-base 16901 df-plusg 16963 df-mulr 16964 df-starv 16965 df-tset 16969 df-ple 16970 df-ds 16972 df-unif 16973 df-rest 17121 df-topn 17122 df-topgen 17142 df-psmet 20577 df-xmet 20578 df-met 20579 df-bl 20580 df-mopn 20581 df-cnfld 20586 df-top 22031 df-topon 22048 df-topsp 22070 df-bases 22084 df-ntr 22159 df-cnp 22367 df-xms 23461 df-ms 23462 df-limc 25018 df-dv 25019 |
This theorem is referenced by: dvbsss 25054 dvres3 25065 dvres3a 25066 dvidlem 25067 dvcnp 25071 dvnff 25075 dvnres 25083 cpnord 25087 dvmulbr 25091 dvaddf 25094 dvmulf 25095 dvcmul 25096 dvcobr 25098 dvcof 25100 dvcjbr 25101 dvrec 25107 dvcnv 25129 dvlipcn 25146 dvlip2 25147 lhop 25168 dvtaylp 25517 ulmdv 25550 pserdv 25576 unbdqndv1 34674 unbdqndv2 34677 knoppndv 34700 fourierdlem80 43686 fourierdlem94 43700 fourierdlem113 43719 |
Copyright terms: Public domain | W3C validator |