Theorem intimafv

Description: The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024)

	Ref	Expression
Assertion	intimafv	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \bigcap F\left[A\right]=\bigcap _{x\in A}F\left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfimafn	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to F\left[A\right]=\left\{y|\exists x\in AF\left(x\right)=y\right\}$$
2	1	inteqd	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \bigcap F\left[A\right]=\bigcap \left\{y|\exists x\in AF\left(x\right)=y\right\}$$
3		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
4	3	rgenw	$$⊢\forall x\in AF\left(x\right)\in \mathrm{V}$$
5		iinabrex	$$⊢\forall x\in AF\left(x\right)\in \mathrm{V}\to \bigcap _{x\in A}F\left(x\right)=\bigcap \left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
6	4 5	ax-mp	$$⊢\bigcap _{x\in A}F\left(x\right)=\bigcap \left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
7		eqcom	$$⊢F\left(x\right)=y\leftrightarrow y=F\left(x\right)$$
8	7	rexbii	$$⊢\exists x\in AF\left(x\right)=y\leftrightarrow \exists x\in Ay=F\left(x\right)$$
9	8	abbii	$$⊢\left\{y|\exists x\in AF\left(x\right)=y\right\}=\left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
10	9	inteqi	$$⊢\bigcap \left\{y|\exists x\in AF\left(x\right)=y\right\}=\bigcap \left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
11	6 10	eqtr4i	$$⊢\bigcap _{x\in A}F\left(x\right)=\bigcap \left\{y|\exists x\in AF\left(x\right)=y\right\}$$
12	2 11	eqtr4di	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \bigcap F\left[A\right]=\bigcap _{x\in A}F\left(x\right)$$