Theorem rescnvimafod

Description: The restriction of a function to a preimage of a class is a function onto the intersection of this class and the range of the function. (Contributed by AV, 13-Sep-2024) (Revised by AV, 29-Sep-2024)

	Ref	Expression
Hypotheses	rescnvimafod.f	$$⊢\phi \to FFnA$$
	rescnvimafod.e	$$⊢\phi \to E=\mathrm{ran}F\cap B$$
	rescnvimafod.d	$$⊢\phi \to D=F^{-1}\left[B\right]$$
Assertion	rescnvimafod	$$⊢\phi \to \left({F\upharpoonright }_D\right):D\underset{onto}{⟶}E$$

Proof

Step	Hyp	Ref	Expression
1		rescnvimafod.f	$$⊢\phi \to FFnA$$
2		rescnvimafod.e	$$⊢\phi \to E=\mathrm{ran}F\cap B$$
3		rescnvimafod.d	$$⊢\phi \to D=F^{-1}\left[B\right]$$
4		cnvimass	$$⊢F^{-1}\left[B\right]\subseteq \mathrm{dom}F$$
5	4	a1i	$$⊢\phi \to F^{-1}\left[B\right]\subseteq \mathrm{dom}F$$
6	1	fndmd	$$⊢\phi \to \mathrm{dom}F=A$$
7	6	eqcomd	$$⊢\phi \to A=\mathrm{dom}F$$
8	5 3 7	3sstr4d	$$⊢\phi \to D\subseteq A$$
9	1 8	fnssresd	$$⊢\phi \to \left({F\upharpoonright }_D\right)FnD$$
10		df-ima	$$⊢F\left[D\right]=\mathrm{ran}\left({F\upharpoonright }_D\right)$$
11	3	imaeq2d	$$⊢\phi \to F\left[D\right]=F\left[F^{-1}\left[B\right]\right]$$
12		fnfun	$$⊢FFnA\to \mathrm{Fun}F$$
13		funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[B\right]\right]=B\cap \mathrm{ran}F$$
14	1 12 13	3syl	$$⊢\phi \to F\left[F^{-1}\left[B\right]\right]=B\cap \mathrm{ran}F$$
15		incom	$$⊢B\cap \mathrm{ran}F=\mathrm{ran}F\cap B$$
16	15	a1i	$$⊢\phi \to B\cap \mathrm{ran}F=\mathrm{ran}F\cap B$$
17	11 14 16	3eqtrd	$$⊢\phi \to F\left[D\right]=\mathrm{ran}F\cap B$$
18	10 17	eqtr3id	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_D\right)=\mathrm{ran}F\cap B$$
19	18 2	eqtr4d	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_D\right)=E$$
20		df-fo	$$⊢\left({F\upharpoonright }_D\right):D\underset{onto}{⟶}E\leftrightarrow \left(\left({F\upharpoonright }_D\right)FnD\wedge \mathrm{ran}\left({F\upharpoonright }_D\right)=E\right)$$
21	9 19 20	sylanbrc	$$⊢\phi \to \left({F\upharpoonright }_D\right):D\underset{onto}{⟶}E$$