Theorem f1oexbi

Description: There is a one-to-one onto function from a set to a second set iff there is a one-to-one onto function from the second set to the first set. (Contributed by Alexander van der Vekens, 30-Sep-2018)

	Ref	Expression
Assertion	f1oexbi	|- ( E. f f : A -1-1-onto-> B <-> E. g g : B -1-1-onto-> A )

Proof

Step	Hyp	Ref	Expression
1		vex	|- f e. _V
2	1	cnvex	|- `' f e. _V
3		f1ocnv	|- ( f : A -1-1-onto-> B -> `' f : B -1-1-onto-> A )
4		f1oeq1	|- ( g = `' f -> ( g : B -1-1-onto-> A <-> `' f : B -1-1-onto-> A ) )
5	4	spcegv	|- ( `' f e. _V -> ( `' f : B -1-1-onto-> A -> E. g g : B -1-1-onto-> A ) )
6	2 3 5	mpsyl	|- ( f : A -1-1-onto-> B -> E. g g : B -1-1-onto-> A )
7	6	exlimiv	|- ( E. f f : A -1-1-onto-> B -> E. g g : B -1-1-onto-> A )
8		vex	|- g e. _V
9	8	cnvex	|- `' g e. _V
10		f1ocnv	|- ( g : B -1-1-onto-> A -> `' g : A -1-1-onto-> B )
11		f1oeq1	|- ( f = `' g -> ( f : A -1-1-onto-> B <-> `' g : A -1-1-onto-> B ) )
12	11	spcegv	|- ( `' g e. _V -> ( `' g : A -1-1-onto-> B -> E. f f : A -1-1-onto-> B ) )
13	9 10 12	mpsyl	|- ( g : B -1-1-onto-> A -> E. f f : A -1-1-onto-> B )
14	13	exlimiv	|- ( E. g g : B -1-1-onto-> A -> E. f f : A -1-1-onto-> B )
15	7 14	impbii	|- ( E. f f : A -1-1-onto-> B <-> E. g g : B -1-1-onto-> A )