# Metamath Proof Explorer

## Theorem dvbss

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
Hypotheses dvcl.s ( 𝜑𝑆 ⊆ ℂ )
dvcl.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
dvcl.a ( 𝜑𝐴𝑆 )
Assertion dvbss ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝐴 )

### Proof

Step Hyp Ref Expression
1 dvcl.s ( 𝜑𝑆 ⊆ ℂ )
2 dvcl.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
3 dvcl.a ( 𝜑𝐴𝑆 )
4 eqid ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
5 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
6 1 2 3 4 5 dvbssntr ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝐴 ) )
7 5 cnfldtop ( TopOpen ‘ ℂfld ) ∈ Top
8 cnex ℂ ∈ V
9 ssexg ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
10 1 8 9 sylancl ( 𝜑𝑆 ∈ V )
11 resttop ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
12 7 10 11 sylancr ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
13 5 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
14 resttopon ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
15 13 1 14 sylancr ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
16 toponuni ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
17 15 16 syl ( 𝜑𝑆 = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
18 3 17 sseqtrd ( 𝜑𝐴 ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
19 eqid ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
20 19 ntrss2 ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top ∧ 𝐴 ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝐴 ) ⊆ 𝐴 )
21 12 18 20 syl2anc ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝐴 ) ⊆ 𝐴 )
22 6 21 sstrd ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝐴 )