Theorem f1ocnv

Description: The converse of a one-to-one onto function is also one-to-one onto. (Contributed by NM, 11-Feb-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		fnrel	|- ( F Fn A -> Rel F )
2		dfrel2	|- ( Rel F <-> `' `' F = F )
3		fneq1	|- ( `' `' F = F -> ( `' `' F Fn A <-> F Fn A ) )
4	3	biimprd	|- ( `' `' F = F -> ( F Fn A -> `' `' F Fn A ) )
5	2 4	sylbi	|- ( Rel F -> ( F Fn A -> `' `' F Fn A ) )
6	1 5	mpcom	|- ( F Fn A -> `' `' F Fn A )
7	6	anim1ci	|- ( ( F Fn A /\ `' F Fn B ) -> ( `' F Fn B /\ `' `' F Fn A ) )
8		dff1o4	|- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
9		dff1o4	|- ( `' F : B -1-1-onto-> A <-> ( `' F Fn B /\ `' `' F Fn A ) )
10	7 8 9	3imtr4i	|- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )