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

Metamath Proof Explorer

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