Metamath Proof Explorer

Theorem f1orescnv

Description: The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion f1orescnv 
|- ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> ( `' F |` P ) : P -1-1-onto-> R )

Proof

Step Hyp Ref Expression
1 f1ocnv 
 |-  ( ( F |` R ) : R -1-1-onto-> P -> `' ( F |` R ) : P -1-1-onto-> R )
2 1 adantl 
 |-  ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> `' ( F |` R ) : P -1-1-onto-> R )
3 funcnvres 
 |-  ( Fun `' F -> `' ( F |` R ) = ( `' F |` ( F " R ) ) )
4 df-ima 
 |-  ( F " R ) = ran ( F |` R )
5 dff1o5 
 |-  ( ( F |` R ) : R -1-1-onto-> P <-> ( ( F |` R ) : R -1-1-> P /\ ran ( F |` R ) = P ) )
6 5 simprbi 
 |-  ( ( F |` R ) : R -1-1-onto-> P -> ran ( F |` R ) = P )
7 4 6 syl5eq 
 |-  ( ( F |` R ) : R -1-1-onto-> P -> ( F " R ) = P )
8 7 reseq2d 
 |-  ( ( F |` R ) : R -1-1-onto-> P -> ( `' F |` ( F " R ) ) = ( `' F |` P ) )
9 3 8 sylan9eq 
 |-  ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> `' ( F |` R ) = ( `' F |` P ) )
10 f1oeq1 
 |-  ( `' ( F |` R ) = ( `' F |` P ) -> ( `' ( F |` R ) : P -1-1-onto-> R <-> ( `' F |` P ) : P -1-1-onto-> R ) )
11 9 10 syl 
 |-  ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> ( `' ( F |` R ) : P -1-1-onto-> R <-> ( `' F |` P ) : P -1-1-onto-> R ) )
12 2 11 mpbid 
 |-  ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> ( `' F |` P ) : P -1-1-onto-> R )