Theorem fcoinver

Description: Build an equivalence relation from a function. Two values are equivalent if they have the same image by the function. See also fcoinvbr . (Contributed by Thierry Arnoux, 3-Jan-2020)

	Ref	Expression
Assertion	fcoinver	$$⊢FFnX\to \left(F^{-1}\circ F\right)\mathrm{Er}X$$

Proof

Step	Hyp	Ref	Expression
1		relco	$$⊢\mathrm{Rel}\left(F^{-1}\circ F\right)$$
2	1	a1i	$$⊢FFnX\to \mathrm{Rel}\left(F^{-1}\circ F\right)$$
3		dmco	$$⊢\mathrm{dom}\left(F^{-1}\circ F\right)=F^{-1}\left[\mathrm{dom}{F}^{-1}\right]$$
4		df-rn	$$⊢\mathrm{ran}F=\mathrm{dom}{F}^{-1}$$
5	4	imaeq2i	$$⊢F^{-1}\left[\mathrm{ran}F\right]=F^{-1}\left[\mathrm{dom}{F}^{-1}\right]$$
6		cnvimarndm	$$⊢F^{-1}\left[\mathrm{ran}F\right]=\mathrm{dom}F$$
7		fndm	$$⊢FFnX\to \mathrm{dom}F=X$$
8	6 7	syl5eq	$$⊢FFnX\to F^{-1}\left[\mathrm{ran}F\right]=X$$
9	5 8	eqtr3id	$$⊢FFnX\to F^{-1}\left[\mathrm{dom}{F}^{-1}\right]=X$$
10	3 9	syl5eq	$$⊢FFnX\to \mathrm{dom}\left(F^{-1}\circ F\right)=X$$
11		cnvco	$$⊢{\left(F^{-1}\circ F\right)}^{-1}=F^{-1}\circ {F^{-1}}^{-1}$$
12		cnvcnvss	$$⊢{F^{-1}}^{-1}\subseteq F$$
13		coss2	$$⊢{F^{-1}}^{-1}\subseteq F\to F^{-1}\circ {F^{-1}}^{-1}\subseteq F^{-1}\circ F$$
14	12 13	ax-mp	$$⊢F^{-1}\circ {F^{-1}}^{-1}\subseteq F^{-1}\circ F$$
15	11 14	eqsstri	$$⊢{\left(F^{-1}\circ F\right)}^{-1}\subseteq F^{-1}\circ F$$
16	15	a1i	$$⊢FFnX\to {\left(F^{-1}\circ F\right)}^{-1}\subseteq F^{-1}\circ F$$
17		coass	$$⊢\left(F^{-1}\circ F\right)\circ \left(F^{-1}\circ F\right)=F^{-1}\circ \left(F\circ \left(F^{-1}\circ F\right)\right)$$
18		coass	$$⊢\left(F\circ F^{-1}\right)\circ F=F\circ \left(F^{-1}\circ F\right)$$
19		fnfun	$$⊢FFnX\to \mathrm{Fun}F$$
20		funcocnv2	$$⊢\mathrm{Fun}F\to F\circ F^{-1}={\mathrm{I}\upharpoonright }_{\mathrm{ran}F}$$
21	19 20	syl	$$⊢FFnX\to F\circ F^{-1}={\mathrm{I}\upharpoonright }_{\mathrm{ran}F}$$
22	21	coeq1d	$$⊢FFnX\to \left(F\circ F^{-1}\right)\circ F=\left({\mathrm{I}\upharpoonright }_{\mathrm{ran}F}\right)\circ F$$
23		dffn3	$$⊢FFnX\leftrightarrow F:X⟶\mathrm{ran}F$$
24		fcoi2	$$⊢F:X⟶\mathrm{ran}F\to \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}F}\right)\circ F=F$$
25	23 24	sylbi	$$⊢FFnX\to \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}F}\right)\circ F=F$$
26	22 25	eqtrd	$$⊢FFnX\to \left(F\circ F^{-1}\right)\circ F=F$$
27	18 26	eqtr3id	$$⊢FFnX\to F\circ \left(F^{-1}\circ F\right)=F$$
28	27	coeq2d	$$⊢FFnX\to F^{-1}\circ \left(F\circ \left(F^{-1}\circ F\right)\right)=F^{-1}\circ F$$
29	17 28	syl5eq	$$⊢FFnX\to \left(F^{-1}\circ F\right)\circ \left(F^{-1}\circ F\right)=F^{-1}\circ F$$
30		ssid	$$⊢F^{-1}\circ F\subseteq F^{-1}\circ F$$
31	29 30	eqsstrdi	$$⊢FFnX\to \left(F^{-1}\circ F\right)\circ \left(F^{-1}\circ F\right)\subseteq F^{-1}\circ F$$
32	16 31	unssd	$$⊢FFnX\to {\left(F^{-1}\circ F\right)}^{-1}\cup \left(\left(F^{-1}\circ F\right)\circ \left(F^{-1}\circ F\right)\right)\subseteq F^{-1}\circ F$$
33		df-er	$$⊢\left(F^{-1}\circ F\right)\mathrm{Er}X\leftrightarrow \left(\mathrm{Rel}\left(F^{-1}\circ F\right)\wedge \mathrm{dom}\left(F^{-1}\circ F\right)=X\wedge {\left(F^{-1}\circ F\right)}^{-1}\cup \left(\left(F^{-1}\circ F\right)\circ \left(F^{-1}\circ F\right)\right)\subseteq F^{-1}\circ F\right)$$
34	2 10 32 33	syl3anbrc	$$⊢FFnX\to \left(F^{-1}\circ F\right)\mathrm{Er}X$$