Theorem reldv

Description: The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	reldv	$$⊢\mathrm{Rel}{F}_S^{\prime }$$

Proof

Step	Hyp	Ref	Expression
1		relxp	$$⊢\mathrm{Rel}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)$$
2	1	rgenw	$$⊢\forall x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)\mathrm{Rel}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)$$
3		reliun	$$⊢\mathrm{Rel}\bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\leftrightarrow \forall x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)\mathrm{Rel}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)$$
4	2 3	mpbir	$$⊢\mathrm{Rel}\bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)$$
5		df-rel	$$⊢\mathrm{Rel}\bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\leftrightarrow \bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
6	4 5	mpbi	$$⊢\bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
7	6	rgenw	$$⊢\forall f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)\bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
8	7	rgenw	$$⊢\forall s\in 𝒫ℂ\forall f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)\bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
9		df-dv	$$⊢\mathrm{D}=\left(s\in 𝒫ℂ,f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)⟼\bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\right)$$
10	9	ovmptss	$$⊢\forall s\in 𝒫ℂ\forall f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)\bigcup _{x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}f\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(\mathrm{dom}f\setminus \left\{x\right\}\right)⟼\frac{f\left(z\right)-f\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\subseteq \mathrm{V}\times \mathrm{V}\to S\mathrm{D}F\subseteq \mathrm{V}\times \mathrm{V}$$
11	8 10	ax-mp	$$⊢S\mathrm{D}F\subseteq \mathrm{V}\times \mathrm{V}$$
12		df-rel	$$⊢\mathrm{Rel}{F}_S^{\prime }\leftrightarrow S\mathrm{D}F\subseteq \mathrm{V}\times \mathrm{V}$$
13	11 12	mpbir	$$⊢\mathrm{Rel}{F}_S^{\prime }$$