Theorem fssres

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004)

	Ref	Expression
Assertion	fssres	$$⊢\left(F:A⟶B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C⟶B$$

Proof

Step	Hyp	Ref	Expression
1		df-f	$$⊢F:A⟶B\leftrightarrow \left(FFnA\wedge \mathrm{ran}F\subseteq B\right)$$
2		fnssres	$$⊢\left(FFnA\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right)FnC$$
3		resss	$$⊢{F\upharpoonright }_C\subseteq F$$
4	3	rnssi	$$⊢\mathrm{ran}\left({F\upharpoonright }_C\right)\subseteq \mathrm{ran}F$$
5		sstr	$$⊢\left(\mathrm{ran}\left({F\upharpoonright }_C\right)\subseteq \mathrm{ran}F\wedge \mathrm{ran}F\subseteq B\right)\to \mathrm{ran}\left({F\upharpoonright }_C\right)\subseteq B$$
6	4 5	mpan	$$⊢\mathrm{ran}F\subseteq B\to \mathrm{ran}\left({F\upharpoonright }_C\right)\subseteq B$$
7	2 6	anim12i	$$⊢\left(\left(FFnA\wedge C\subseteq A\right)\wedge \mathrm{ran}F\subseteq B\right)\to \left(\left({F\upharpoonright }_C\right)FnC\wedge \mathrm{ran}\left({F\upharpoonright }_C\right)\subseteq B\right)$$
8	7	an32s	$$⊢\left(\left(FFnA\wedge \mathrm{ran}F\subseteq B\right)\wedge C\subseteq A\right)\to \left(\left({F\upharpoonright }_C\right)FnC\wedge \mathrm{ran}\left({F\upharpoonright }_C\right)\subseteq B\right)$$
9	1 8	sylanb	$$⊢\left(F:A⟶B\wedge C\subseteq A\right)\to \left(\left({F\upharpoonright }_C\right)FnC\wedge \mathrm{ran}\left({F\upharpoonright }_C\right)\subseteq B\right)$$
10		df-f	$$⊢\left({F\upharpoonright }_C\right):C⟶B\leftrightarrow \left(\left({F\upharpoonright }_C\right)FnC\wedge \mathrm{ran}\left({F\upharpoonright }_C\right)\subseteq B\right)$$
11	9 10	sylibr	$$⊢\left(F:A⟶B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C⟶B$$