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