Metamath Proof Explorer

Theorem dvbssntr

Description: The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

		Ref	Expression
	Hypotheses	dvcl.s	$⊢ φ \to S \subseteq ℂ$
		dvcl.f	$⊢ φ \to F : A ⟶ ℂ$
		dvcl.a	$⊢ φ \to A \subseteq S$
		dvbssntr.j	$⊢ J = K ↾_{𝑡} S$
		dvbssntr.k	$⊢ K = TopOpen (ℂ_{fld})$
	Assertion	dvbssntr	$⊢ φ \to dom F_{S}^{'} \subseteq int (J) (A)$

Proof

Step	Hyp	Ref	Expression
1		dvcl.s	$⊢ φ \to S \subseteq ℂ$
2		dvcl.f	$⊢ φ \to F : A ⟶ ℂ$
3		dvcl.a	$⊢ φ \to A \subseteq S$
4		dvbssntr.j	$⊢ J = K ↾_{𝑡} S$
5		dvbssntr.k	$⊢ K = TopOpen (ℂ_{fld})$
6	4 5	dvfval	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (S D F = ⋃_{x \in int (J) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \land S D F \subseteq int (J) (A) \times ℂ)$
7	1 2 3 6	syl3anc	$⊢ φ \to (S D F = ⋃_{x \in int (J) (A)} (\{x\} \times ((z \in (A ∖ \{x\}) ⟼ \frac{F (z) - F (x)}{z - x}) {lim}_{ℂ} x)) \land S D F \subseteq int (J) (A) \times ℂ)$
8		dmss	$⊢ S D F \subseteq int (J) (A) \times ℂ \to dom F_{S}^{'} \subseteq dom (int (J) (A) \times ℂ)$
9	7 8	simpl2im	$⊢ φ \to dom F_{S}^{'} \subseteq dom (int (J) (A) \times ℂ)$
10		dmxpss	$⊢ dom (int (J) (A) \times ℂ) \subseteq int (J) (A)$
11	9 10	sstrdi	$⊢ φ \to dom F_{S}^{'} \subseteq int (J) (A)$