# Metamath Proof Explorer

## 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}↾}_{{A}}$

### Proof

Step Hyp Ref Expression
1 f1orel ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to \mathrm{Rel}{F}$
2 dfrel2 ${⊢}\mathrm{Rel}{F}↔{{{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}↾}_{{A}}$
7 5 6 syl ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}\circ {{{F}}^{-1}}^{-1}={\mathrm{I}↾}_{{A}}$
8 4 7 eqtr3d ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}\circ {F}={\mathrm{I}↾}_{{A}}$