Theorem funimacnv

Description: The image of the preimage of a function. (Contributed by NM, 25-May-2004)

	Ref	Expression
Assertion	funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[A\right]\right]=A\cap \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢F\left[F^{-1}\left[A\right]\right]=\mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[A\right]}\right)$$
2		funcnvres2	$$⊢\mathrm{Fun}F\to {\left({F^{-1}\upharpoonright }_A\right)}^{-1}={F\upharpoonright }_{F^{-1}\left[A\right]}$$
3	2	rneqd	$$⊢\mathrm{Fun}F\to \mathrm{ran}{\left({F^{-1}\upharpoonright }_A\right)}^{-1}=\mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[A\right]}\right)$$
4	1 3	eqtr4id	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[A\right]\right]=\mathrm{ran}{\left({F^{-1}\upharpoonright }_A\right)}^{-1}$$
5		df-rn	$$⊢\mathrm{ran}F=\mathrm{dom}{F}^{-1}$$
6	5	ineq2i	$$⊢A\cap \mathrm{ran}F=A\cap \mathrm{dom}{F}^{-1}$$
7		dmres	$$⊢\mathrm{dom}\left({F^{-1}\upharpoonright }_A\right)=A\cap \mathrm{dom}{F}^{-1}$$
8		dfdm4	$$⊢\mathrm{dom}\left({F^{-1}\upharpoonright }_A\right)=\mathrm{ran}{\left({F^{-1}\upharpoonright }_A\right)}^{-1}$$
9	6 7 8	3eqtr2ri	$$⊢\mathrm{ran}{\left({F^{-1}\upharpoonright }_A\right)}^{-1}=A\cap \mathrm{ran}F$$
10	4 9	eqtrdi	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[A\right]\right]=A\cap \mathrm{ran}F$$