Theorem dvmptrecl

Description: Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	dvmptrecl.s	$$⊢\phi \to S\subseteq ℝ$$
	dvmptrecl.a	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℝ$$
	dvmptrecl.v	$$⊢\left(\phi \wedge x\in S\right)\to B\in V$$
	dvmptrecl.b	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\left(x\in S⟼B\right)$$
Assertion	dvmptrecl	$$⊢\left(\phi \wedge x\in S\right)\to B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		dvmptrecl.s	$$⊢\phi \to S\subseteq ℝ$$
2		dvmptrecl.a	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℝ$$
3		dvmptrecl.v	$$⊢\left(\phi \wedge x\in S\right)\to B\in V$$
4		dvmptrecl.b	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\left(x\in S⟼B\right)$$
5	2	fmpttd	$$⊢\phi \to \left(x\in S⟼A\right):S⟶ℝ$$
6		dvfre	$$⊢\left(\left(x\in S⟼A\right):S⟶ℝ\wedge S\subseteq ℝ\right)\to \frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}:\mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}⟶ℝ$$
7	5 1 6	syl2anc	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}:\mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}⟶ℝ$$
8	4	dmeqd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\mathrm{dom}\left(x\in S⟼B\right)$$
9	3	ralrimiva	$$⊢\phi \to \forall x\in SB\in V$$
10		dmmptg	$$⊢\forall x\in SB\in V\to \mathrm{dom}\left(x\in S⟼B\right)=S$$
11	9 10	syl	$$⊢\phi \to \mathrm{dom}\left(x\in S⟼B\right)=S$$
12	8 11	eqtrd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=S$$
13	4 12	feq12d	$$⊢\phi \to \left(\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}:\mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}⟶ℝ\leftrightarrow \left(x\in S⟼B\right):S⟶ℝ\right)$$
14	7 13	mpbid	$$⊢\phi \to \left(x\in S⟼B\right):S⟶ℝ$$
15	14	fvmptelcdm	$$⊢\left(\phi \wedge x\in S\right)\to B\in ℝ$$