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		funcnvres2	$$⊢\mathrm{Fun}F\to {\left({F^{-1}\upharpoonright }_A\right)}^{-1}={F\upharpoonright }_{F^{-1}\left[A\right]}$$
2	1	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)$$
3		df-ima	$$⊢F\left[F^{-1}\left[A\right]\right]=\mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[A\right]}\right)$$
4	2 3	syl6reqr	$$⊢\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	syl6eq	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[A\right]\right]=A\cap \mathrm{ran}F$$