# Metamath Proof Explorer

## Theorem funcnvres

Description: The converse of a restricted function. (Contributed by NM, 27-Mar-1998)

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

### Proof

Step Hyp Ref Expression
1 df-ima ${⊢}{F}\left[{A}\right]=\mathrm{ran}\left({{F}↾}_{{A}}\right)$
2 df-rn ${⊢}\mathrm{ran}\left({{F}↾}_{{A}}\right)=\mathrm{dom}{\left({{F}↾}_{{A}}\right)}^{-1}$
3 1 2 eqtri ${⊢}{F}\left[{A}\right]=\mathrm{dom}{\left({{F}↾}_{{A}}\right)}^{-1}$
4 3 reseq2i ${⊢}{{{F}}^{-1}↾}_{{F}\left[{A}\right]}={{{F}}^{-1}↾}_{\mathrm{dom}{\left({{F}↾}_{{A}}\right)}^{-1}}$
5 resss ${⊢}{{F}↾}_{{A}}\subseteq {F}$
6 cnvss ${⊢}{{F}↾}_{{A}}\subseteq {F}\to {\left({{F}↾}_{{A}}\right)}^{-1}\subseteq {{F}}^{-1}$
7 5 6 ax-mp ${⊢}{\left({{F}↾}_{{A}}\right)}^{-1}\subseteq {{F}}^{-1}$
8 funssres ${⊢}\left(\mathrm{Fun}{{F}}^{-1}\wedge {\left({{F}↾}_{{A}}\right)}^{-1}\subseteq {{F}}^{-1}\right)\to {{{F}}^{-1}↾}_{\mathrm{dom}{\left({{F}↾}_{{A}}\right)}^{-1}}={\left({{F}↾}_{{A}}\right)}^{-1}$
9 7 8 mpan2 ${⊢}\mathrm{Fun}{{F}}^{-1}\to {{{F}}^{-1}↾}_{\mathrm{dom}{\left({{F}↾}_{{A}}\right)}^{-1}}={\left({{F}↾}_{{A}}\right)}^{-1}$
10 4 9 syl5req ${⊢}\mathrm{Fun}{{F}}^{-1}\to {\left({{F}↾}_{{A}}\right)}^{-1}={{{F}}^{-1}↾}_{{F}\left[{A}\right]}$