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