Metamath Proof Explorer


Theorem funimacnv

Description: The image of the preimage of a function. (Contributed by NM, 25-May-2004)

Ref Expression
Assertion funimacnv ( Fun 𝐹 → ( 𝐹 “ ( 𝐹𝐴 ) ) = ( 𝐴 ∩ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 df-ima ( 𝐹 “ ( 𝐹𝐴 ) ) = ran ( 𝐹 ↾ ( 𝐹𝐴 ) )
2 funcnvres2 ( Fun 𝐹 ( 𝐹𝐴 ) = ( 𝐹 ↾ ( 𝐹𝐴 ) ) )
3 2 rneqd ( Fun 𝐹 → ran ( 𝐹𝐴 ) = ran ( 𝐹 ↾ ( 𝐹𝐴 ) ) )
4 1 3 eqtr4id ( Fun 𝐹 → ( 𝐹 “ ( 𝐹𝐴 ) ) = ran ( 𝐹𝐴 ) )
5 df-rn ran 𝐹 = dom 𝐹
6 5 ineq2i ( 𝐴 ∩ ran 𝐹 ) = ( 𝐴 ∩ dom 𝐹 )
7 dmres dom ( 𝐹𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
8 dfdm4 dom ( 𝐹𝐴 ) = ran ( 𝐹𝐴 )
9 6 7 8 3eqtr2ri ran ( 𝐹𝐴 ) = ( 𝐴 ∩ ran 𝐹 )
10 4 9 eqtrdi ( Fun 𝐹 → ( 𝐹 “ ( 𝐹𝐴 ) ) = ( 𝐴 ∩ ran 𝐹 ) )