Metamath Proof Explorer

Theorem funcnvres

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

Ref Expression
Assertion funcnvres 
|- ( Fun `' F -> `' ( F |` A ) = ( `' F |` ( F " A ) ) )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( F " A ) = ran ( F |` A )
2 df-rn 
 |-  ran ( F |` A ) = dom `' ( F |` A )
3 1 2 eqtri 
 |-  ( F " A ) = dom `' ( F |` A )
4 3 reseq2i 
 |-  ( `' F |` ( F " A ) ) = ( `' F |` dom `' ( F |` A ) )
5 resss 
 |-  ( F |` A ) C_ F
6 cnvss 
 |-  ( ( F |` A ) C_ F -> `' ( F |` A ) C_ `' F )
7 5 6 ax-mp 
 |-  `' ( F |` A ) C_ `' F
8 funssres 
 |-  ( ( Fun `' F /\ `' ( F |` A ) C_ `' F ) -> ( `' F |` dom `' ( F |` A ) ) = `' ( F |` A ) )
9 7 8 mpan2 
 |-  ( Fun `' F -> ( `' F |` dom `' ( F |` A ) ) = `' ( F |` A ) )
10 4 9 syl5req 
 |-  ( Fun `' F -> `' ( F |` A ) = ( `' F |` ( F " A ) ) )