Theorem fnresin

Description: Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017)

	Ref	Expression
Assertion	fnresin	$$⊢FFnA\to \left({F\upharpoonright }_B\right)Fn\left(A\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnresin1	$$⊢FFnA\to \left({F\upharpoonright }_{\left(A\cap B\right)}\right)Fn\left(A\cap B\right)$$
2		resindi	$$⊢{F\upharpoonright }_{\left(A\cap B\right)}=\left({F\upharpoonright }_A\right)\cap \left({F\upharpoonright }_B\right)$$
3		fnresdm	$$⊢FFnA\to {F\upharpoonright }_A=F$$
4	3	ineq1d	$$⊢FFnA\to \left({F\upharpoonright }_A\right)\cap \left({F\upharpoonright }_B\right)=F\cap \left({F\upharpoonright }_B\right)$$
5		incom	$$⊢\left({F\upharpoonright }_B\right)\cap F=F\cap \left({F\upharpoonright }_B\right)$$
6		resss	$$⊢{F\upharpoonright }_B\subseteq F$$
7		df-ss	$$⊢{F\upharpoonright }_B\subseteq F\leftrightarrow \left({F\upharpoonright }_B\right)\cap F={F\upharpoonright }_B$$
8	6 7	mpbi	$$⊢\left({F\upharpoonright }_B\right)\cap F={F\upharpoonright }_B$$
9	5 8	eqtr3i	$$⊢F\cap \left({F\upharpoonright }_B\right)={F\upharpoonright }_B$$
10	4 9	eqtrdi	$$⊢FFnA\to \left({F\upharpoonright }_A\right)\cap \left({F\upharpoonright }_B\right)={F\upharpoonright }_B$$
11	2 10	syl5eq	$$⊢FFnA\to {F\upharpoonright }_{\left(A\cap B\right)}={F\upharpoonright }_B$$
12	11	fneq1d	$$⊢FFnA\to \left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right)Fn\left(A\cap B\right)\leftrightarrow \left({F\upharpoonright }_B\right)Fn\left(A\cap B\right)\right)$$
13	1 12	mpbid	$$⊢FFnA\to \left({F\upharpoonright }_B\right)Fn\left(A\cap B\right)$$