Metamath Proof Explorer


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 𝐹 → ( 𝐹𝐴 ) = ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 inpreima ( Fun 𝐹 → ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) )
2 funforn ( Fun 𝐹𝐹 : dom 𝐹onto→ ran 𝐹 )
3 fof ( 𝐹 : dom 𝐹onto→ ran 𝐹𝐹 : dom 𝐹 ⟶ ran 𝐹 )
4 2 3 sylbi ( Fun 𝐹𝐹 : dom 𝐹 ⟶ ran 𝐹 )
5 fimacnv ( 𝐹 : dom 𝐹 ⟶ ran 𝐹 → ( 𝐹 “ ran 𝐹 ) = dom 𝐹 )
6 4 5 syl ( Fun 𝐹 → ( 𝐹 “ ran 𝐹 ) = dom 𝐹 )
7 6 ineq2d ( Fun 𝐹 → ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) = ( ( 𝐹𝐴 ) ∩ dom 𝐹 ) )
8 cnvresima ( ( 𝐹 ↾ dom 𝐹 ) “ 𝐴 ) = ( ( 𝐹𝐴 ) ∩ dom 𝐹 )
9 resdm2 ( 𝐹 ↾ dom 𝐹 ) = 𝐹
10 funrel ( Fun 𝐹 → Rel 𝐹 )
11 dfrel2 ( Rel 𝐹 𝐹 = 𝐹 )
12 10 11 sylib ( Fun 𝐹 𝐹 = 𝐹 )
13 9 12 eqtrid ( Fun 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
14 13 cnveqd ( Fun 𝐹 ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
15 14 imaeq1d ( Fun 𝐹 → ( ( 𝐹 ↾ dom 𝐹 ) “ 𝐴 ) = ( 𝐹𝐴 ) )
16 8 15 eqtr3id ( Fun 𝐹 → ( ( 𝐹𝐴 ) ∩ dom 𝐹 ) = ( 𝐹𝐴 ) )
17 1 7 16 3eqtrrd ( Fun 𝐹 → ( 𝐹𝐴 ) = ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )