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	syl5eq	⊢ ( 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 𝐹 ) ) )