# Metamath Proof Explorer

## Theorem cnvresid

Description: Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007)

Ref Expression
Assertion cnvresid ${⊢}{\left({\mathrm{I}↾}_{{A}}\right)}^{-1}={\mathrm{I}↾}_{{A}}$

### Proof

Step Hyp Ref Expression
1 cnvi ${⊢}{\mathrm{I}}^{-1}=\mathrm{I}$
2 1 eqcomi ${⊢}\mathrm{I}={\mathrm{I}}^{-1}$
3 funi ${⊢}\mathrm{Fun}\mathrm{I}$
4 funeq ${⊢}\mathrm{I}={\mathrm{I}}^{-1}\to \left(\mathrm{Fun}\mathrm{I}↔\mathrm{Fun}{\mathrm{I}}^{-1}\right)$
5 3 4 mpbii ${⊢}\mathrm{I}={\mathrm{I}}^{-1}\to \mathrm{Fun}{\mathrm{I}}^{-1}$
6 funcnvres ${⊢}\mathrm{Fun}{\mathrm{I}}^{-1}\to {\left({\mathrm{I}↾}_{{A}}\right)}^{-1}={{\mathrm{I}}^{-1}↾}_{\mathrm{I}\left[{A}\right]}$
7 imai ${⊢}\mathrm{I}\left[{A}\right]={A}$
8 1 7 reseq12i ${⊢}{{\mathrm{I}}^{-1}↾}_{\mathrm{I}\left[{A}\right]}={\mathrm{I}↾}_{{A}}$
9 6 8 syl6eq ${⊢}\mathrm{Fun}{\mathrm{I}}^{-1}\to {\left({\mathrm{I}↾}_{{A}}\right)}^{-1}={\mathrm{I}↾}_{{A}}$
10 2 5 9 mp2b ${⊢}{\left({\mathrm{I}↾}_{{A}}\right)}^{-1}={\mathrm{I}↾}_{{A}}$