This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )