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

Metamath Proof Explorer

Theorem funcnvres2

Description: The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by NM, 4-May-2005)

Ref Expression
Assertion funcnvres2 ⊢ Fun ⁡ F → F -1 ↾ A -1 = F ↾ F -1 A

Proof

Step Hyp Ref Expression
1 funcnvcnv ⊢ Fun ⁡ F → Fun ⁡ F -1 -1
2 funcnvres ⊢ Fun ⁡ F -1 -1 → F -1 ↾ A -1 = F -1 -1 ↾ F -1 A
3 1 2 syl ⊢ Fun ⁡ F → F -1 ↾ A -1 = F -1 -1 ↾ F -1 A
4 funrel ⊢ Fun ⁡ F → Rel ⁡ F
5 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
6 4 5 sylib ⊢ Fun ⁡ F → F -1 -1 = F
7 6 reseq1d ⊢ Fun ⁡ F → F -1 -1 ↾ F -1 A = F ↾ F -1 A
8 3 7 eqtrd ⊢ Fun ⁡ F → F -1 ↾ A -1 = F ↾ F -1 A