Theorem fimacnvinrn2

Description: Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017)

	Ref	Expression
Assertion	fimacnvinrn2	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		inass	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) = ( 𝐴 ∩ ( 𝐵 ∩ ran 𝐹 ) )
2		sseqin2	⊢ ( ran 𝐹 ⊆ 𝐵 ↔ ( 𝐵 ∩ ran 𝐹 ) = ran 𝐹 )
3	2	biimpi	⊢ ( ran 𝐹 ⊆ 𝐵 → ( 𝐵 ∩ ran 𝐹 ) = ran 𝐹 )
4	3	adantl	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( 𝐵 ∩ ran 𝐹 ) = ran 𝐹 )
5	4	ineq2d	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( 𝐴 ∩ ( 𝐵 ∩ ran 𝐹 ) ) = ( 𝐴 ∩ ran 𝐹 ) )
6	1 5	eqtrid	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) = ( 𝐴 ∩ ran 𝐹 ) )
7	6	imaeq2d	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) ) = ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )
8		fimacnvinrn	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ◡ 𝐹 “ ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) ) )
9	8	adantr	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ◡ 𝐹 “ ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) ) )
10		fimacnvinrn	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )
11	10	adantr	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )
12	7 9 11	3eqtr4rd	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) )