Theorem foimacnv

Description: A reverse version of f1imacnv . (Contributed by Jeff Hankins, 16-Jul-2009)

	Ref	Expression
Assertion	foimacnv	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to F\left[F^{-1}\left[C\right]\right]=C$$

Proof

Step	Hyp	Ref	Expression
1		resima	$$⊢\left({F\upharpoonright }_{F^{-1}\left[C\right]}\right)\left[F^{-1}\left[C\right]\right]=F\left[F^{-1}\left[C\right]\right]$$
2		fofun	$$⊢F:A\underset{onto}{⟶}B\to \mathrm{Fun}F$$
3	2	adantr	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to \mathrm{Fun}F$$
4		funcnvres2	$$⊢\mathrm{Fun}F\to {\left({F^{-1}\upharpoonright }_C\right)}^{-1}={F\upharpoonright }_{F^{-1}\left[C\right]}$$
5	3 4	syl	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to {\left({F^{-1}\upharpoonright }_C\right)}^{-1}={F\upharpoonright }_{F^{-1}\left[C\right]}$$
6	5	imaeq1d	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to {\left({F^{-1}\upharpoonright }_C\right)}^{-1}\left[F^{-1}\left[C\right]\right]=\left({F\upharpoonright }_{F^{-1}\left[C\right]}\right)\left[F^{-1}\left[C\right]\right]$$
7		resss	$$⊢{F^{-1}\upharpoonright }_C\subseteq F^{-1}$$
8		cnvss	$$⊢{F^{-1}\upharpoonright }_C\subseteq F^{-1}\to {\left({F^{-1}\upharpoonright }_C\right)}^{-1}\subseteq {F^{-1}}^{-1}$$
9	7 8	ax-mp	$$⊢{\left({F^{-1}\upharpoonright }_C\right)}^{-1}\subseteq {F^{-1}}^{-1}$$
10		cnvcnvss	$$⊢{F^{-1}}^{-1}\subseteq F$$
11	9 10	sstri	$$⊢{\left({F^{-1}\upharpoonright }_C\right)}^{-1}\subseteq F$$
12		funss	$$⊢{\left({F^{-1}\upharpoonright }_C\right)}^{-1}\subseteq F\to \left(\mathrm{Fun}F\to \mathrm{Fun}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}\right)$$
13	11 2 12	mpsyl	$$⊢F:A\underset{onto}{⟶}B\to \mathrm{Fun}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}$$
14	13	adantr	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to \mathrm{Fun}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}$$
15		df-ima	$$⊢F^{-1}\left[C\right]=\mathrm{ran}\left({F^{-1}\upharpoonright }_C\right)$$
16		df-rn	$$⊢\mathrm{ran}\left({F^{-1}\upharpoonright }_C\right)=\mathrm{dom}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}$$
17	15 16	eqtr2i	$$⊢\mathrm{dom}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}=F^{-1}\left[C\right]$$
18		df-fn	$$⊢{\left({F^{-1}\upharpoonright }_C\right)}^{-1}Fn{F}^{-1}\left[C\right]\leftrightarrow \left(\mathrm{Fun}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}\wedge \mathrm{dom}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}=F^{-1}\left[C\right]\right)$$
19	14 17 18	sylanblrc	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to {\left({F^{-1}\upharpoonright }_C\right)}^{-1}Fn{F}^{-1}\left[C\right]$$
20		dfdm4	$$⊢\mathrm{dom}\left({F^{-1}\upharpoonright }_C\right)=\mathrm{ran}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}$$
21		forn	$$⊢F:A\underset{onto}{⟶}B\to \mathrm{ran}F=B$$
22	21	sseq2d	$$⊢F:A\underset{onto}{⟶}B\to \left(C\subseteq \mathrm{ran}F\leftrightarrow C\subseteq B\right)$$
23	22	biimpar	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to C\subseteq \mathrm{ran}F$$
24		df-rn	$$⊢\mathrm{ran}F=\mathrm{dom}{F}^{-1}$$
25	23 24	sseqtrdi	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to C\subseteq \mathrm{dom}{F}^{-1}$$
26		ssdmres	$$⊢C\subseteq \mathrm{dom}{F}^{-1}\leftrightarrow \mathrm{dom}\left({F^{-1}\upharpoonright }_C\right)=C$$
27	25 26	sylib	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to \mathrm{dom}\left({F^{-1}\upharpoonright }_C\right)=C$$
28	20 27	eqtr3id	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to \mathrm{ran}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}=C$$
29		df-fo	$$⊢{\left({F^{-1}\upharpoonright }_C\right)}^{-1}:F^{-1}\left[C\right]\underset{onto}{⟶}C\leftrightarrow \left({\left({F^{-1}\upharpoonright }_C\right)}^{-1}Fn{F}^{-1}\left[C\right]\wedge \mathrm{ran}{\left({F^{-1}\upharpoonright }_C\right)}^{-1}=C\right)$$
30	19 28 29	sylanbrc	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to {\left({F^{-1}\upharpoonright }_C\right)}^{-1}:F^{-1}\left[C\right]\underset{onto}{⟶}C$$
31		foima	$$⊢{\left({F^{-1}\upharpoonright }_C\right)}^{-1}:F^{-1}\left[C\right]\underset{onto}{⟶}C\to {\left({F^{-1}\upharpoonright }_C\right)}^{-1}\left[F^{-1}\left[C\right]\right]=C$$
32	30 31	syl	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to {\left({F^{-1}\upharpoonright }_C\right)}^{-1}\left[F^{-1}\left[C\right]\right]=C$$
33	6 32	eqtr3d	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to \left({F\upharpoonright }_{F^{-1}\left[C\right]}\right)\left[F^{-1}\left[C\right]\right]=C$$
34	1 33	eqtr3id	$$⊢\left(F:A\underset{onto}{⟶}B\wedge C\subseteq B\right)\to F\left[F^{-1}\left[C\right]\right]=C$$