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

Metamath Proof Explorer

Theorem funimacnv

Description: The image of the preimage of a function. (Contributed by NM, 25-May-2004)

Ref Expression
Assertion funimacnv ⊢ Fun ⁡ F → F F -1 A = A ∩ ran ⁡ F

Proof

Step Hyp Ref Expression
1 df-ima ⊢ F F -1 A = ran ⁡ F ↾ F -1 A
2 funcnvres2 ⊢ Fun ⁡ F → F -1 ↾ A -1 = F ↾ F -1 A
3 2 rneqd ⊢ Fun ⁡ F → ran ⁡ F -1 ↾ A -1 = ran ⁡ F ↾ F -1 A
4 1 3 eqtr4id ⊢ Fun ⁡ F → F F -1 A = ran ⁡ F -1 ↾ A -1
5 df-rn ⊢ ran ⁡ F = dom ⁡ F -1
6 5 ineq2i ⊢ A ∩ ran ⁡ F = A ∩ dom ⁡ F -1
7 dmres ⊢ dom ⁡ F -1 ↾ A = A ∩ dom ⁡ F -1
8 dfdm4 ⊢ dom ⁡ F -1 ↾ A = ran ⁡ F -1 ↾ A -1
9 6 7 8 3eqtr2ri ⊢ ran ⁡ F -1 ↾ A -1 = A ∩ ran ⁡ F
10 4 9 eqtrdi ⊢ Fun ⁡ F → F F -1 A = A ∩ ran ⁡ F