# Metamath Proof Explorer

## Theorem funcnvres2

Description: The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by NM, 4-May-2005)

Ref Expression
Assertion funcnvres2 ${⊢}\mathrm{Fun}{F}\to {\left({{{F}}^{-1}↾}_{{A}}\right)}^{-1}={{F}↾}_{{{F}}^{-1}\left[{A}\right]}$

### Proof

Step Hyp Ref Expression
1 funcnvcnv ${⊢}\mathrm{Fun}{F}\to \mathrm{Fun}{{{F}}^{-1}}^{-1}$
2 funcnvres ${⊢}\mathrm{Fun}{{{F}}^{-1}}^{-1}\to {\left({{{F}}^{-1}↾}_{{A}}\right)}^{-1}={{{{F}}^{-1}}^{-1}↾}_{{{F}}^{-1}\left[{A}\right]}$
3 1 2 syl ${⊢}\mathrm{Fun}{F}\to {\left({{{F}}^{-1}↾}_{{A}}\right)}^{-1}={{{{F}}^{-1}}^{-1}↾}_{{{F}}^{-1}\left[{A}\right]}$
4 funrel ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
5 dfrel2 ${⊢}\mathrm{Rel}{F}↔{{{F}}^{-1}}^{-1}={F}$
6 4 5 sylib ${⊢}\mathrm{Fun}{F}\to {{{F}}^{-1}}^{-1}={F}$
7 6 reseq1d ${⊢}\mathrm{Fun}{F}\to {{{{F}}^{-1}}^{-1}↾}_{{{F}}^{-1}\left[{A}\right]}={{F}↾}_{{{F}}^{-1}\left[{A}\right]}$
8 3 7 eqtrd ${⊢}\mathrm{Fun}{F}\to {\left({{{F}}^{-1}↾}_{{A}}\right)}^{-1}={{F}↾}_{{{F}}^{-1}\left[{A}\right]}$