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}^{'} \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		df-dv	$⊢ D = (s \in 𝒫 ℂ, f \in (ℂ ↑_{𝑝𝑚} s) ⟼ ⋃_{x \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} s) (dom f)} (\{x\} \times ((z \in (dom f ∖ \{x\}) ⟼ \frac{f (z) - f (x)}{z - x}) {lim}_{ℂ} x)))$
2	1	reldmmpo	$⊢ Rel dom D$
3		df-rel	$⊢ Rel dom D \leftrightarrow dom D \subseteq V \times V$
4	2 3	mpbi	$⊢ dom D \subseteq V \times V$
5	4	sseli	$⊢ ⟨S, F⟩ \in dom D \to ⟨S, F⟩ \in (V \times V)$
6		opelxp1	$⊢ ⟨S, F⟩ \in (V \times V) \to S \in V$
7	5 6	syl	$⊢ ⟨S, F⟩ \in dom D \to S \in V$
8		opeq1	$⊢ s = S \to ⟨s, F⟩ = ⟨S, F⟩$
9	8	eleq1d	$⊢ s = S \to (⟨s, F⟩ \in dom D \leftrightarrow ⟨S, F⟩ \in dom D)$
10		eleq1	$⊢ s = S \to (s \in 𝒫 ℂ \leftrightarrow S \in 𝒫 ℂ)$
11		oveq2	$⊢ s = S \to ℂ ↑_{𝑝𝑚} s = ℂ ↑_{𝑝𝑚} S$
12	11	eleq2d	$⊢ s = S \to (F \in (ℂ ↑_{𝑝𝑚} s) \leftrightarrow F \in (ℂ ↑_{𝑝𝑚} S))$
13	10 12	anbi12d	$⊢ s = S \to ((s \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} s)) \leftrightarrow (S \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)))$
14	9 13	imbi12d	$⊢ s = S \to ((⟨s, F⟩ \in dom D \to (s \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} s))) \leftrightarrow (⟨S, F⟩ \in dom D \to (S \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} S))))$
15	1	dmmpossx	$⊢ dom D \subseteq ⋃_{s \in 𝒫 ℂ} (\{s\} \times (ℂ ↑_{𝑝𝑚} s))$
16	15	sseli	$⊢ ⟨s, F⟩ \in dom D \to ⟨s, F⟩ \in ⋃_{s \in 𝒫 ℂ} (\{s\} \times (ℂ ↑_{𝑝𝑚} s))$
17		opeliunxp	$⊢ ⟨s, F⟩ \in ⋃_{s \in 𝒫 ℂ} (\{s\} \times (ℂ ↑_{𝑝𝑚} s)) \leftrightarrow (s \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} s))$
18	16 17	sylib	$⊢ ⟨s, F⟩ \in dom D \to (s \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} s))$
19	14 18	vtoclg	$⊢ S \in V \to (⟨S, F⟩ \in dom D \to (S \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)))$
20	7 19	mpcom	$⊢ ⟨S, F⟩ \in dom D \to (S \in 𝒫 ℂ \land F \in (ℂ ↑_{𝑝𝑚} S))$
21	20	simpld	$⊢ ⟨S, F⟩ \in dom D \to S \in 𝒫 ℂ$
22	21	elpwid	$⊢ ⟨S, F⟩ \in dom D \to S \subseteq ℂ$
23	20	simprd	$⊢ ⟨S, F⟩ \in dom D \to F \in (ℂ ↑_{𝑝𝑚} S)$
24		cnex	$⊢ ℂ \in V$
25		elpm2g	$⊢ (ℂ \in V \land S \in 𝒫 ℂ) \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
26	24 21 25	sylancr	$⊢ ⟨S, F⟩ \in dom D \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
27	23 26	mpbid	$⊢ ⟨S, F⟩ \in dom D \to (F : dom F ⟶ ℂ \land dom F \subseteq S)$
28	27	simpld	$⊢ ⟨S, F⟩ \in dom D \to F : dom F ⟶ ℂ$
29	27	simprd	$⊢ ⟨S, F⟩ \in dom D \to dom F \subseteq S$
30	22 28 29	dvbss	$⊢ ⟨S, F⟩ \in dom D \to dom F_{S}^{'} \subseteq dom F$
31	30 29	sstrd	$⊢ ⟨S, F⟩ \in dom D \to dom F_{S}^{'} \subseteq S$
32		df-ov	$⊢ S D F = D (⟨S, F⟩)$
33		ndmfv	$⊢ \neg ⟨S, F⟩ \in dom D \to D (⟨S, F⟩) = \emptyset$
34	32 33	syl5eq	$⊢ \neg ⟨S, F⟩ \in dom D \to S D F = \emptyset$
35	34	dmeqd	$⊢ \neg ⟨S, F⟩ \in dom D \to dom F_{S}^{'} = dom \emptyset$
36		dm0	$⊢ dom \emptyset = \emptyset$
37	35 36	eqtrdi	$⊢ \neg ⟨S, F⟩ \in dom D \to dom F_{S}^{'} = \emptyset$
38		0ss	$⊢ \emptyset \subseteq S$
39	37 38	eqsstrdi	$⊢ \neg ⟨S, F⟩ \in dom D \to dom F_{S}^{'} \subseteq S$
40	31 39	pm2.61i	$⊢ dom F_{S}^{'} \subseteq S$

Metamath Proof Explorer

Theorem dvbsss

Proof