Theorem f1ococnv1

Description: The composition of a one-to-one onto function's converse and itself equals the identity relation restricted to the function's domain. (Contributed by NM, 13-Dec-2003)

	Ref	Expression
Assertion	f1ococnv1	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}\circ F={\mathrm{I}\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		f1orel	$$⊢F:A\underset{1-1\; onto}{⟶}B\to \mathrm{Rel}F$$
2		dfrel2	$$⊢\mathrm{Rel}F\leftrightarrow {F^{-1}}^{-1}=F$$
3	1 2	sylib	$$⊢F:A\underset{1-1\; onto}{⟶}B\to {F^{-1}}^{-1}=F$$
4	3	coeq2d	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}\circ {F^{-1}}^{-1}=F^{-1}\circ F$$
5		f1ocnv	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}:B\underset{1-1\; onto}{⟶}A$$
6		f1ococnv2	$$⊢F^{-1}:B\underset{1-1\; onto}{⟶}A\to F^{-1}\circ {F^{-1}}^{-1}={\mathrm{I}\upharpoonright }_A$$
7	5 6	syl	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}\circ {F^{-1}}^{-1}={\mathrm{I}\upharpoonright }_A$$
8	4 7	eqtr3d	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}\circ F={\mathrm{I}\upharpoonright }_A$$