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	syl5eq	⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ 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 𝐹 ) ⊆ 𝑆