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 biimpi 
 |-  ( ran F C_ B -> ( B i^i ran F ) = ran F )
4 3 adantl 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( B i^i ran F ) = ran F )
5 4 ineq2d 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( A i^i ( B i^i ran F ) ) = ( A i^i ran F ) )
6 1 5 eqtrid 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( ( A i^i B ) i^i ran F ) = ( A i^i ran F ) )
7 6 imaeq2d 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( `' F " ( ( A i^i B ) i^i ran F ) ) = ( `' F " ( A i^i ran F ) ) )
8 fimacnvinrn 
 |-  ( Fun F -> ( `' F " ( A i^i B ) ) = ( `' F " ( ( A i^i B ) i^i ran F ) ) )
9 8 adantr 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( `' F " ( A i^i B ) ) = ( `' F " ( ( A i^i B ) i^i ran F ) ) )
10 fimacnvinrn 
 |-  ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )
11 10 adantr 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )
12 7 9 11 3eqtr4rd 
 |-  ( ( Fun F /\ ran F C_ B ) -> ( `' F " A ) = ( `' F " ( A i^i B ) ) )