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
|- ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )

Proof

Step Hyp Ref Expression
1 inpreima
 |-  ( Fun F -> ( `' F " ( A i^i ran F ) ) = ( ( `' F " A ) i^i ( `' F " ran F ) ) )
2 funforn
 |-  ( Fun F <-> F : dom F -onto-> ran F )
3 fof
 |-  ( F : dom F -onto-> ran F -> F : dom F --> ran F )
4 2 3 sylbi
 |-  ( Fun F -> F : dom F --> ran F )
5 fimacnv
 |-  ( F : dom F --> ran F -> ( `' F " ran F ) = dom F )
6 4 5 syl
 |-  ( Fun F -> ( `' F " ran F ) = dom F )
7 6 ineq2d
 |-  ( Fun F -> ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( ( `' F " A ) i^i dom F ) )
8 cnvresima
 |-  ( `' ( F |` dom F ) " A ) = ( ( `' F " A ) i^i dom F )
9 resdm2
 |-  ( F |` dom F ) = `' `' F
10 funrel
 |-  ( Fun F -> Rel F )
11 dfrel2
 |-  ( Rel F <-> `' `' F = F )
12 10 11 sylib
 |-  ( Fun F -> `' `' F = F )
13 9 12 eqtrid
 |-  ( Fun F -> ( F |` dom F ) = F )
14 13 cnveqd
 |-  ( Fun F -> `' ( F |` dom F ) = `' F )
15 14 imaeq1d
 |-  ( Fun F -> ( `' ( F |` dom F ) " A ) = ( `' F " A ) )
16 8 15 eqtr3id
 |-  ( Fun F -> ( ( `' F " A ) i^i dom F ) = ( `' F " A ) )
17 1 7 16 3eqtrrd
 |-  ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )