Theorem resin

Description: The restriction of a one-to-one onto function to an intersection maps onto the intersection of the images. (Contributed by Paul Chapman, 11-Apr-2009)

	Ref	Expression
Assertion	resin	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\wedge \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\right)\to \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\cap D$$

Proof

Step	Hyp	Ref	Expression
1		resdif	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\wedge \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\right)\to \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{1-1\; onto}{⟶}C\setminus D$$
2		f1ofo	$$⊢\left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{1-1\; onto}{⟶}C\setminus D\to \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}C\setminus D$$
3	1 2	syl	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\wedge \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\right)\to \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}C\setminus D$$
4		resdif	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\wedge \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}C\setminus D\right)\to \left({F\upharpoonright }_{\left(A\setminus \left(A\setminus B\right)\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)$$
5	3 4	syld3an3	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\wedge \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\right)\to \left({F\upharpoonright }_{\left(A\setminus \left(A\setminus B\right)\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)$$
6		dfin4	$$⊢C\cap D=C\setminus \left(C\setminus D\right)$$
7		f1oeq3	$$⊢C\cap D=C\setminus \left(C\setminus D\right)\to \left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\cap D\leftrightarrow \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)\right)$$
8	6 7	ax-mp	$$⊢\left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\cap D\leftrightarrow \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)$$
9		dfin4	$$⊢A\cap B=A\setminus \left(A\setminus B\right)$$
10		f1oeq2	$$⊢A\cap B=A\setminus \left(A\setminus B\right)\to \left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)\leftrightarrow \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)\right)$$
11	9 10	ax-mp	$$⊢\left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)\leftrightarrow \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)$$
12	9	reseq2i	$$⊢{F\upharpoonright }_{\left(A\cap B\right)}={F\upharpoonright }_{\left(A\setminus \left(A\setminus B\right)\right)}$$
13		f1oeq1	$$⊢{F\upharpoonright }_{\left(A\cap B\right)}={F\upharpoonright }_{\left(A\setminus \left(A\setminus B\right)\right)}\to \left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus \left(A\setminus B\right)\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)\right)$$
14	12 13	ax-mp	$$⊢\left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus \left(A\setminus B\right)\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)$$
15	8 11 14	3bitrri	$$⊢\left({F\upharpoonright }_{\left(A\setminus \left(A\setminus B\right)\right)}\right):A\setminus \left(A\setminus B\right)\underset{1-1\; onto}{⟶}C\setminus \left(C\setminus D\right)\leftrightarrow \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\cap D$$
16	5 15	sylib	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\wedge \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\right)\to \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B\underset{1-1\; onto}{⟶}C\cap D$$