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