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 eqtrid
 |-  ( ( 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 9 f1oeq1d
 |-  ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> ( `' ( F |` R ) : P -1-1-onto-> R <-> ( `' F |` P ) : P -1-1-onto-> R ) )
11 2 10 mpbid
 |-  ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> ( `' F |` P ) : P -1-1-onto-> R )