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