Theorem resfvresima

Description: The value of the function value of a restriction for a function restricted to the image of the restricting subset. (Contributed by AV, 6-Mar-2021)

	Ref	Expression
Hypotheses	resfvresima.f	$$⊢\phi \to \mathrm{Fun}F$$
	resfvresima.s	$$⊢\phi \to S\subseteq \mathrm{dom}F$$
	resfvresima.x	$$⊢\phi \to X\in S$$
Assertion	resfvresima	$$⊢\phi \to \left({H\upharpoonright }_{F\left[S\right]}\right)\left(\left({F\upharpoonright }_S\right)\left(X\right)\right)=H\left(F\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		resfvresima.f	$$⊢\phi \to \mathrm{Fun}F$$
2		resfvresima.s	$$⊢\phi \to S\subseteq \mathrm{dom}F$$
3		resfvresima.x	$$⊢\phi \to X\in S$$
4	3	fvresd	$$⊢\phi \to \left({F\upharpoonright }_S\right)\left(X\right)=F\left(X\right)$$
5	4	fveq2d	$$⊢\phi \to \left({H\upharpoonright }_{F\left[S\right]}\right)\left(\left({F\upharpoonright }_S\right)\left(X\right)\right)=\left({H\upharpoonright }_{F\left[S\right]}\right)\left(F\left(X\right)\right)$$
6	1 2	jca	$$⊢\phi \to \left(\mathrm{Fun}F\wedge S\subseteq \mathrm{dom}F\right)$$
7		funfvima2	$$⊢\left(\mathrm{Fun}F\wedge S\subseteq \mathrm{dom}F\right)\to \left(X\in S\to F\left(X\right)\in F\left[S\right]\right)$$
8	6 3 7	sylc	$$⊢\phi \to F\left(X\right)\in F\left[S\right]$$
9	8	fvresd	$$⊢\phi \to \left({H\upharpoonright }_{F\left[S\right]}\right)\left(F\left(X\right)\right)=H\left(F\left(X\right)\right)$$
10	5 9	eqtrd	$$⊢\phi \to \left({H\upharpoonright }_{F\left[S\right]}\right)\left(\left({F\upharpoonright }_S\right)\left(X\right)\right)=H\left(F\left(X\right)\right)$$