# Metamath Proof Explorer

## Theorem fimacnvinrn

Description: Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion fimacnvinrn ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[{A}\right]={{F}}^{-1}\left[{A}\cap \mathrm{ran}{F}\right]$

### Proof

Step Hyp Ref Expression
1 inpreima ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[{A}\cap \mathrm{ran}{F}\right]={{F}}^{-1}\left[{A}\right]\cap {{F}}^{-1}\left[\mathrm{ran}{F}\right]$
2 funforn ${⊢}\mathrm{Fun}{F}↔{F}:\mathrm{dom}{F}\underset{onto}{⟶}\mathrm{ran}{F}$
3 fof ${⊢}{F}:\mathrm{dom}{F}\underset{onto}{⟶}\mathrm{ran}{F}\to {F}:\mathrm{dom}{F}⟶\mathrm{ran}{F}$
4 2 3 sylbi ${⊢}\mathrm{Fun}{F}\to {F}:\mathrm{dom}{F}⟶\mathrm{ran}{F}$
5 fimacnv ${⊢}{F}:\mathrm{dom}{F}⟶\mathrm{ran}{F}\to {{F}}^{-1}\left[\mathrm{ran}{F}\right]=\mathrm{dom}{F}$
6 4 5 syl ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[\mathrm{ran}{F}\right]=\mathrm{dom}{F}$
7 6 ineq2d ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[{A}\right]\cap {{F}}^{-1}\left[\mathrm{ran}{F}\right]={{F}}^{-1}\left[{A}\right]\cap \mathrm{dom}{F}$
8 cnvresima ${⊢}{\left({{F}↾}_{\mathrm{dom}{F}}\right)}^{-1}\left[{A}\right]={{F}}^{-1}\left[{A}\right]\cap \mathrm{dom}{F}$
9 resdm2 ${⊢}{{F}↾}_{\mathrm{dom}{F}}={{{F}}^{-1}}^{-1}$
10 funrel ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
11 dfrel2 ${⊢}\mathrm{Rel}{F}↔{{{F}}^{-1}}^{-1}={F}$
12 10 11 sylib ${⊢}\mathrm{Fun}{F}\to {{{F}}^{-1}}^{-1}={F}$
13 9 12 syl5eq ${⊢}\mathrm{Fun}{F}\to {{F}↾}_{\mathrm{dom}{F}}={F}$
14 13 cnveqd ${⊢}\mathrm{Fun}{F}\to {\left({{F}↾}_{\mathrm{dom}{F}}\right)}^{-1}={{F}}^{-1}$
15 14 imaeq1d ${⊢}\mathrm{Fun}{F}\to {\left({{F}↾}_{\mathrm{dom}{F}}\right)}^{-1}\left[{A}\right]={{F}}^{-1}\left[{A}\right]$
16 8 15 syl5eqr ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[{A}\right]\cap \mathrm{dom}{F}={{F}}^{-1}\left[{A}\right]$
17 1 7 16 3eqtrrd ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[{A}\right]={{F}}^{-1}\left[{A}\cap \mathrm{ran}{F}\right]$