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	bilani	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( 𝐵 ∩ ran 𝐹 ) = ran 𝐹 )
4	3	ineq2d	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( 𝐴 ∩ ( 𝐵 ∩ ran 𝐹 ) ) = ( 𝐴 ∩ ran 𝐹 ) )
5	1 4	eqtrid	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) = ( 𝐴 ∩ ran 𝐹 ) )
6	5	imaeq2d	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) ) = ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )
7		fimacnvinrn	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ◡ 𝐹 “ ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) ) )
8	7	adantr	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ◡ 𝐹 “ ( ( 𝐴 ∩ 𝐵 ) ∩ ran 𝐹 ) ) )
9		fimacnvinrn	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )
10	9	adantr	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )
11	6 8 10	3eqtr4rd	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) )