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 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	syl5ib	|- ( 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 ) )