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

Metamath Proof Explorer

Theorem funimacnv

Description: The image of the preimage of a function. (Contributed by NM, 25-May-2004)

Ref Expression
Assertion funimacnv 
|- ( Fun F -> ( F " ( `' F " A ) ) = ( A i^i ran F ) )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( F " ( `' F " A ) ) = ran ( F |` ( `' F " A ) )
2 funcnvres2 
 |-  ( Fun F -> `' ( `' F |` A ) = ( F |` ( `' F " A ) ) )
3 2 rneqd 
 |-  ( Fun F -> ran `' ( `' F |` A ) = ran ( F |` ( `' F " A ) ) )
4 1 3 eqtr4id 
 |-  ( Fun F -> ( F " ( `' F " A ) ) = ran `' ( `' F |` A ) )
5 df-rn 
 |-  ran F = dom `' F
6 5 ineq2i 
 |-  ( A i^i ran F ) = ( A i^i dom `' F )
7 dmres 
 |-  dom ( `' F |` A ) = ( A i^i dom `' F )
8 dfdm4 
 |-  dom ( `' F |` A ) = ran `' ( `' F |` A )
9 6 7 8 3eqtr2ri 
 |-  ran `' ( `' F |` A ) = ( A i^i ran F )
10 4 9 eqtrdi 
 |-  ( Fun F -> ( F " ( `' F " A ) ) = ( A i^i ran F ) )