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 𝐹 ) ⊆ 𝐴 )