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

Metamath Proof Explorer

Theorem f1ocnvb

Description: A relation is a one-to-one onto function iff its converse is a one-to-one onto function with domain and codomain/range interchanged. (Contributed by NM, 8-Dec-2003)

Ref Expression
Assertion f1ocnvb 
|- ( Rel F -> ( F : A -1-1-onto-> B <-> `' F : B -1-1-onto-> A ) )

Proof

Step Hyp Ref Expression
1 f1ocnv 
 |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
2 f1ocnv 
 |-  ( `' F : B -1-1-onto-> A -> `' `' F : A -1-1-onto-> B )
3 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
4 f1oeq1 
 |-  ( `' `' F = F -> ( `' `' F : A -1-1-onto-> B <-> F : A -1-1-onto-> B ) )
5 3 4 sylbi 
 |-  ( Rel F -> ( `' `' F : A -1-1-onto-> B <-> F : A -1-1-onto-> B ) )
6 2 5 imbitrid 
 |-  ( Rel F -> ( `' F : B -1-1-onto-> A -> F : A -1-1-onto-> B ) )
7 1 6 impbid2 
 |-  ( Rel F -> ( F : A -1-1-onto-> B <-> `' F : B -1-1-onto-> A ) )