Metamath Proof Explorer

Theorem fimacnvinrn2

Description: Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017)

Ref Expression
Assertion fimacnvinrn2 
|- ( ( Fun F /\ ran F C_ B ) -> ( `' F " A ) = ( `' F " ( A i^i B ) ) )

Proof

Step Hyp Ref Expression
1 inass 
 |-  ( ( A i^i B ) i^i ran F ) = ( A i^i ( B i^i ran F ) )
2 sseqin2 
 |-  ( ran F C_ B <-> ( B i^i ran F ) = ran F )
3 2 bilani 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( B i^i ran F ) = ran F )
4 3 ineq2d 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( A i^i ( B i^i ran F ) ) = ( A i^i ran F ) )
5 1 4 eqtrid 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( ( A i^i B ) i^i ran F ) = ( A i^i ran F ) )
6 5 imaeq2d 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( `' F " ( ( A i^i B ) i^i ran F ) ) = ( `' F " ( A i^i ran F ) ) )
7 fimacnvinrn 
 |-  ( Fun F -> ( `' F " ( A i^i B ) ) = ( `' F " ( ( A i^i B ) i^i ran F ) ) )
8 7 adantr 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( `' F " ( A i^i B ) ) = ( `' F " ( ( A i^i B ) i^i ran F ) ) )
9 fimacnvinrn 
 |-  ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )
10 9 adantr 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )
11 6 8 10 3eqtr4rd 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( `' F " A ) = ( `' F " ( A i^i B ) ) )