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 ⁡ F → F -1 A = F -1 A ∩ ran ⁡ F

Proof

Step Hyp Ref Expression
1 inpreima ⊢ Fun ⁡ F → F -1 A ∩ ran ⁡ F = F -1 A ∩ F -1 ran ⁡ F
2 funforn ⊢ Fun ⁡ F ↔ F : dom ⁡ F ⟶ onto ran ⁡ F
3 fof ⊢ F : dom ⁡ F ⟶ onto ran ⁡ F → F : dom ⁡ F ⟶ ran ⁡ F
4 2 3 sylbi ⊢ Fun ⁡ F → F : dom ⁡ F ⟶ ran ⁡ F
5 fimacnv ⊢ F : dom ⁡ F ⟶ ran ⁡ F → F -1 ran ⁡ F = dom ⁡ F
6 4 5 syl ⊢ Fun ⁡ F → F -1 ran ⁡ F = dom ⁡ F
7 6 ineq2d ⊢ Fun ⁡ F → F -1 A ∩ F -1 ran ⁡ F = F -1 A ∩ dom ⁡ F
8 cnvresima ⊢ F ↾ dom ⁡ F -1 A = F -1 A ∩ dom ⁡ F
9 resdm2 ⊢ F ↾ dom ⁡ F = F -1 -1
10 funrel ⊢ Fun ⁡ F → Rel ⁡ F
11 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
12 10 11 sylib ⊢ Fun ⁡ F → F -1 -1 = F
13 9 12 eqtrid ⊢ Fun ⁡ F → F ↾ dom ⁡ F = F
14 13 cnveqd ⊢ Fun ⁡ F → F ↾ dom ⁡ F -1 = F -1
15 14 imaeq1d ⊢ Fun ⁡ F → F ↾ dom ⁡ F -1 A = F -1 A
16 8 15 eqtr3id ⊢ Fun ⁡ F → F -1 A ∩ dom ⁡ F = F -1 A
17 1 7 16 3eqtrrd ⊢ Fun ⁡ F → F -1 A = F -1 A ∩ ran ⁡ F