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

Metamath Proof Explorer

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 )