This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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