Metamath Proof Explorer


Theorem funcnvres

Description: The converse of a restricted function. (Contributed by NM, 27-Mar-1998)

Ref Expression
Assertion funcnvres ( Fun 𝐹 ( 𝐹𝐴 ) = ( 𝐹 ↾ ( 𝐹𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 df-ima ( 𝐹𝐴 ) = ran ( 𝐹𝐴 )
2 df-rn ran ( 𝐹𝐴 ) = dom ( 𝐹𝐴 )
3 1 2 eqtri ( 𝐹𝐴 ) = dom ( 𝐹𝐴 )
4 3 reseq2i ( 𝐹 ↾ ( 𝐹𝐴 ) ) = ( 𝐹 ↾ dom ( 𝐹𝐴 ) )
5 resss ( 𝐹𝐴 ) ⊆ 𝐹
6 cnvss ( ( 𝐹𝐴 ) ⊆ 𝐹 ( 𝐹𝐴 ) ⊆ 𝐹 )
7 5 6 ax-mp ( 𝐹𝐴 ) ⊆ 𝐹
8 funssres ( ( Fun 𝐹 ( 𝐹𝐴 ) ⊆ 𝐹 ) → ( 𝐹 ↾ dom ( 𝐹𝐴 ) ) = ( 𝐹𝐴 ) )
9 7 8 mpan2 ( Fun 𝐹 → ( 𝐹 ↾ dom ( 𝐹𝐴 ) ) = ( 𝐹𝐴 ) )
10 4 9 eqtr2id ( Fun 𝐹 ( 𝐹𝐴 ) = ( 𝐹 ↾ ( 𝐹𝐴 ) ) )