Theorem funcnvres

Description: The converse of a restricted function. (Contributed by NM, 27-Mar-1998)

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

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢F\left[A\right]=\mathrm{ran}\left({F\upharpoonright }_A\right)$$
2		df-rn	$$⊢\mathrm{ran}\left({F\upharpoonright }_A\right)=\mathrm{dom}{\left({F\upharpoonright }_A\right)}^{-1}$$
3	1 2	eqtri	$$⊢F\left[A\right]=\mathrm{dom}{\left({F\upharpoonright }_A\right)}^{-1}$$
4	3	reseq2i	$$⊢{F^{-1}\upharpoonright }_{F\left[A\right]}={F^{-1}\upharpoonright }_{\mathrm{dom}{\left({F\upharpoonright }_A\right)}^{-1}}$$
5		resss	$$⊢{F\upharpoonright }_A\subseteq F$$
6		cnvss	$$⊢{F\upharpoonright }_A\subseteq F\to {\left({F\upharpoonright }_A\right)}^{-1}\subseteq F^{-1}$$
7	5 6	ax-mp	$$⊢{\left({F\upharpoonright }_A\right)}^{-1}\subseteq F^{-1}$$
8		funssres	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge {\left({F\upharpoonright }_A\right)}^{-1}\subseteq F^{-1}\right)\to {F^{-1}\upharpoonright }_{\mathrm{dom}{\left({F\upharpoonright }_A\right)}^{-1}}={\left({F\upharpoonright }_A\right)}^{-1}$$
9	7 8	mpan2	$$⊢\mathrm{Fun}{F}^{-1}\to {F^{-1}\upharpoonright }_{\mathrm{dom}{\left({F\upharpoonright }_A\right)}^{-1}}={\left({F\upharpoonright }_A\right)}^{-1}$$
10	4 9	syl5req	$$⊢\mathrm{Fun}{F}^{-1}\to {\left({F\upharpoonright }_A\right)}^{-1}={F^{-1}\upharpoonright }_{F\left[A\right]}$$