Theorem fimacnvinrn

Description: Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 21-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		inpreima	$$⊢\mathrm{Fun}F\to F^{-1}\left[A\cap \mathrm{ran}F\right]=F^{-1}\left[A\right]\cap F^{-1}\left[\mathrm{ran}F\right]$$
2		funforn	$$⊢\mathrm{Fun}F\leftrightarrow F:\mathrm{dom}F\underset{onto}{⟶}\mathrm{ran}F$$
3		fof	$$⊢F:\mathrm{dom}F\underset{onto}{⟶}\mathrm{ran}F\to F:\mathrm{dom}F⟶\mathrm{ran}F$$
4	2 3	sylbi	$$⊢\mathrm{Fun}F\to F:\mathrm{dom}F⟶\mathrm{ran}F$$
5		fimacnv	$$⊢F:\mathrm{dom}F⟶\mathrm{ran}F\to F^{-1}\left[\mathrm{ran}F\right]=\mathrm{dom}F$$
6	4 5	syl	$$⊢\mathrm{Fun}F\to F^{-1}\left[\mathrm{ran}F\right]=\mathrm{dom}F$$
7	6	ineq2d	$$⊢\mathrm{Fun}F\to F^{-1}\left[A\right]\cap F^{-1}\left[\mathrm{ran}F\right]=F^{-1}\left[A\right]\cap \mathrm{dom}F$$
8		cnvresima	$$⊢{\left({F\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}\left[A\right]=F^{-1}\left[A\right]\cap \mathrm{dom}F$$
9		resdm2	$$⊢{F\upharpoonright }_{\mathrm{dom}F}={F^{-1}}^{-1}$$
10		funrel	$$⊢\mathrm{Fun}F\to \mathrm{Rel}F$$
11		dfrel2	$$⊢\mathrm{Rel}F\leftrightarrow {F^{-1}}^{-1}=F$$
12	10 11	sylib	$$⊢\mathrm{Fun}F\to {F^{-1}}^{-1}=F$$
13	9 12	eqtrid	$$⊢\mathrm{Fun}F\to {F\upharpoonright }_{\mathrm{dom}F}=F$$
14	13	cnveqd	$$⊢\mathrm{Fun}F\to {\left({F\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=F^{-1}$$
15	14	imaeq1d	$$⊢\mathrm{Fun}F\to {\left({F\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}\left[A\right]=F^{-1}\left[A\right]$$
16	8 15	eqtr3id	$$⊢\mathrm{Fun}F\to F^{-1}\left[A\right]\cap \mathrm{dom}F=F^{-1}\left[A\right]$$
17	1 7 16	3eqtrrd	$$⊢\mathrm{Fun}F\to F^{-1}\left[A\right]=F^{-1}\left[A\cap \mathrm{ran}F\right]$$