Step 
Hyp 
Ref 
Expression 
1 

dfima 
 ( 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 

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