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

Metamath Proof Explorer

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 𝐹 ⊆ 𝐵 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) )