Theorem f1imacnv

Description: Preimage of an image. (Contributed by NM, 30-Sep-2004)

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

Proof

Step	Hyp	Ref	Expression
1		resima	$$⊢\left({F^{-1}\upharpoonright }_{F\left[C\right]}\right)\left[F\left[C\right]\right]=F^{-1}\left[F\left[C\right]\right]$$
2		df-f1	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \mathrm{Fun}{F}^{-1}\right)$$
3	2	simprbi	$$⊢F:A\underset{1-1}{⟶}B\to \mathrm{Fun}{F}^{-1}$$
4	3	adantr	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \mathrm{Fun}{F}^{-1}$$
5		funcnvres	$$⊢\mathrm{Fun}{F}^{-1}\to {\left({F\upharpoonright }_C\right)}^{-1}={F^{-1}\upharpoonright }_{F\left[C\right]}$$
6	4 5	syl	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to {\left({F\upharpoonright }_C\right)}^{-1}={F^{-1}\upharpoonright }_{F\left[C\right]}$$
7	6	imaeq1d	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to {\left({F\upharpoonright }_C\right)}^{-1}\left[F\left[C\right]\right]=\left({F^{-1}\upharpoonright }_{F\left[C\right]}\right)\left[F\left[C\right]\right]$$
8		f1ores	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]$$
9		f1ocnv	$$⊢\left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]\to {\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{1-1\; onto}{⟶}C$$
10	8 9	syl	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to {\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{1-1\; onto}{⟶}C$$
11		imadmrn	$$⊢{\left({F\upharpoonright }_C\right)}^{-1}\left[\mathrm{dom}{\left({F\upharpoonright }_C\right)}^{-1}\right]=\mathrm{ran}{\left({F\upharpoonright }_C\right)}^{-1}$$
12		f1odm	$$⊢{\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{1-1\; onto}{⟶}C\to \mathrm{dom}{\left({F\upharpoonright }_C\right)}^{-1}=F\left[C\right]$$
13	12	imaeq2d	$$⊢{\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{1-1\; onto}{⟶}C\to {\left({F\upharpoonright }_C\right)}^{-1}\left[\mathrm{dom}{\left({F\upharpoonright }_C\right)}^{-1}\right]={\left({F\upharpoonright }_C\right)}^{-1}\left[F\left[C\right]\right]$$
14		f1ofo	$$⊢{\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{1-1\; onto}{⟶}C\to {\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{onto}{⟶}C$$
15		forn	$$⊢{\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{onto}{⟶}C\to \mathrm{ran}{\left({F\upharpoonright }_C\right)}^{-1}=C$$
16	14 15	syl	$$⊢{\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{1-1\; onto}{⟶}C\to \mathrm{ran}{\left({F\upharpoonright }_C\right)}^{-1}=C$$
17	11 13 16	3eqtr3a	$$⊢{\left({F\upharpoonright }_C\right)}^{-1}:F\left[C\right]\underset{1-1\; onto}{⟶}C\to {\left({F\upharpoonright }_C\right)}^{-1}\left[F\left[C\right]\right]=C$$
18	10 17	syl	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to {\left({F\upharpoonright }_C\right)}^{-1}\left[F\left[C\right]\right]=C$$
19	7 18	eqtr3d	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \left({F^{-1}\upharpoonright }_{F\left[C\right]}\right)\left[F\left[C\right]\right]=C$$
20	1 19	syl5eqr	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to F^{-1}\left[F\left[C\right]\right]=C$$