Theorem resdif

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

	Ref	Expression
Assertion	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$$

Proof

Step	Hyp	Ref	Expression
1		fofun	$$⊢\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\to \mathrm{Fun}\left({F\upharpoonright }_A\right)$$
2		difss	$$⊢A\setminus B\subseteq A$$
3		fof	$$⊢\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\to \left({F\upharpoonright }_A\right):A⟶C$$
4	3	fdmd	$$⊢\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\to \mathrm{dom}\left({F\upharpoonright }_A\right)=A$$
5	2 4	sseqtrrid	$$⊢\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\to A\setminus B\subseteq \mathrm{dom}\left({F\upharpoonright }_A\right)$$
6		fores	$$⊢\left(\mathrm{Fun}\left({F\upharpoonright }_A\right)\wedge A\setminus B\subseteq \mathrm{dom}\left({F\upharpoonright }_A\right)\right)\to \left({\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]$$
7	1 5 6	syl2anc	$$⊢\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\to \left({\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]$$
8		resres	$$⊢{\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}={F\upharpoonright }_{\left(A\cap \left(A\setminus B\right)\right)}$$
9		indif	$$⊢A\cap \left(A\setminus B\right)=A\setminus B$$
10	9	reseq2i	$$⊢{F\upharpoonright }_{\left(A\cap \left(A\setminus B\right)\right)}={F\upharpoonright }_{\left(A\setminus B\right)}$$
11	8 10	eqtri	$$⊢{\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}={F\upharpoonright }_{\left(A\setminus B\right)}$$
12		foeq1	$$⊢{\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}={F\upharpoonright }_{\left(A\setminus B\right)}\to \left(\left({\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]\right)$$
13	11 12	ax-mp	$$⊢\left({\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]$$
14	11	rneqi	$$⊢\mathrm{ran}\left({\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}\right)=\mathrm{ran}\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)$$
15		df-ima	$$⊢\left({F\upharpoonright }_A\right)\left[A\setminus B\right]=\mathrm{ran}\left({\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}\right)$$
16		df-ima	$$⊢F\left[A\setminus B\right]=\mathrm{ran}\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)$$
17	14 15 16	3eqtr4i	$$⊢\left({F\upharpoonright }_A\right)\left[A\setminus B\right]=F\left[A\setminus B\right]$$
18		foeq3	$$⊢\left({F\upharpoonright }_A\right)\left[A\setminus B\right]=F\left[A\setminus B\right]\to \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}F\left[A\setminus B\right]\right)$$
19	17 18	ax-mp	$$⊢\left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}F\left[A\setminus B\right]$$
20	13 19	bitri	$$⊢\left({\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}\left({F\upharpoonright }_A\right)\left[A\setminus B\right]\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}F\left[A\setminus B\right]$$
21	7 20	sylib	$$⊢\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\to \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}F\left[A\setminus B\right]$$
22		funres11	$$⊢\mathrm{Fun}{F}^{-1}\to \mathrm{Fun}{\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)}^{-1}$$
23		dff1o3	$$⊢\left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{1-1\; onto}{⟶}F\left[A\setminus B\right]\leftrightarrow \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}F\left[A\setminus B\right]\wedge \mathrm{Fun}{\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)}^{-1}\right)$$
24	23	biimpri	$$⊢\left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{onto}{⟶}F\left[A\setminus B\right]\wedge \mathrm{Fun}{\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)}^{-1}\right)\to \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{1-1\; onto}{⟶}F\left[A\setminus B\right]$$
25	21 22 24	syl2anr	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\right)\to \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{1-1\; onto}{⟶}F\left[A\setminus B\right]$$
26	25	3adant3	$$⊢\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}{⟶}F\left[A\setminus B\right]$$
27		df-ima	$$⊢F\left[A\right]=\mathrm{ran}\left({F\upharpoonright }_A\right)$$
28		forn	$$⊢\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\to \mathrm{ran}\left({F\upharpoonright }_A\right)=C$$
29	27 28	eqtrid	$$⊢\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\to F\left[A\right]=C$$
30		df-ima	$$⊢F\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)$$
31		forn	$$⊢\left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\to \mathrm{ran}\left({F\upharpoonright }_B\right)=D$$
32	30 31	eqtrid	$$⊢\left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\to F\left[B\right]=D$$
33	29 32	anim12i	$$⊢\left(\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\wedge \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\right)\to \left(F\left[A\right]=C\wedge F\left[B\right]=D\right)$$
34		imadif	$$⊢\mathrm{Fun}{F}^{-1}\to F\left[A\setminus B\right]=F\left[A\right]\setminus F\left[B\right]$$
35		difeq12	$$⊢\left(F\left[A\right]=C\wedge F\left[B\right]=D\right)\to F\left[A\right]\setminus F\left[B\right]=C\setminus D$$
36	34 35	sylan9eq	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left(F\left[A\right]=C\wedge F\left[B\right]=D\right)\right)\to F\left[A\setminus B\right]=C\setminus D$$
37	33 36	sylan2	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left(\left({F\upharpoonright }_A\right):A\underset{onto}{⟶}C\wedge \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}D\right)\right)\to F\left[A\setminus B\right]=C\setminus D$$
38	37	3impb	$$⊢\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 F\left[A\setminus B\right]=C\setminus D$$
39	38	f1oeq3d	$$⊢\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(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{1-1\; onto}{⟶}F\left[A\setminus B\right]\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B\underset{1-1\; onto}{⟶}C\setminus D\right)$$
40	26 39	mpbid	$$⊢\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$$