Theorem funcnvres2

Description: The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by NM, 4-May-2005)

	Ref	Expression
Assertion	funcnvres2	$$⊢\mathrm{Fun}F\to {\left({F^{-1}\upharpoonright }_A\right)}^{-1}={F\upharpoonright }_{F^{-1}\left[A\right]}$$

Proof

Step	Hyp	Ref	Expression
1		funcnvcnv	$$⊢\mathrm{Fun}F\to \mathrm{Fun}{F^{-1}}^{-1}$$
2		funcnvres	$$⊢\mathrm{Fun}{F^{-1}}^{-1}\to {\left({F^{-1}\upharpoonright }_A\right)}^{-1}={{F^{-1}}^{-1}\upharpoonright }_{F^{-1}\left[A\right]}$$
3	1 2	syl	$$⊢\mathrm{Fun}F\to {\left({F^{-1}\upharpoonright }_A\right)}^{-1}={{F^{-1}}^{-1}\upharpoonright }_{F^{-1}\left[A\right]}$$
4		funrel	$$⊢\mathrm{Fun}F\to \mathrm{Rel}F$$
5		dfrel2	$$⊢\mathrm{Rel}F\leftrightarrow {F^{-1}}^{-1}=F$$
6	4 5	sylib	$$⊢\mathrm{Fun}F\to {F^{-1}}^{-1}=F$$
7	6	reseq1d	$$⊢\mathrm{Fun}F\to {{F^{-1}}^{-1}\upharpoonright }_{F^{-1}\left[A\right]}={F\upharpoonright }_{F^{-1}\left[A\right]}$$
8	3 7	eqtrd	$$⊢\mathrm{Fun}F\to {\left({F^{-1}\upharpoonright }_A\right)}^{-1}={F\upharpoonright }_{F^{-1}\left[A\right]}$$