Metamath Proof Explorer


Theorem xpcomf1o

Description: The canonical bijection from ( A X. B ) to ( B X. A ) . (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypothesis xpcomf1o.1
|- F = ( x e. ( A X. B ) |-> U. `' { x } )
Assertion xpcomf1o
|- F : ( A X. B ) -1-1-onto-> ( B X. A )

Proof

Step Hyp Ref Expression
1 xpcomf1o.1
 |-  F = ( x e. ( A X. B ) |-> U. `' { x } )
2 relxp
 |-  Rel ( A X. B )
3 cnvf1o
 |-  ( Rel ( A X. B ) -> ( x e. ( A X. B ) |-> U. `' { x } ) : ( A X. B ) -1-1-onto-> `' ( A X. B ) )
4 2 3 ax-mp
 |-  ( x e. ( A X. B ) |-> U. `' { x } ) : ( A X. B ) -1-1-onto-> `' ( A X. B )
5 f1oeq1
 |-  ( F = ( x e. ( A X. B ) |-> U. `' { x } ) -> ( F : ( A X. B ) -1-1-onto-> `' ( A X. B ) <-> ( x e. ( A X. B ) |-> U. `' { x } ) : ( A X. B ) -1-1-onto-> `' ( A X. B ) ) )
6 1 5 ax-mp
 |-  ( F : ( A X. B ) -1-1-onto-> `' ( A X. B ) <-> ( x e. ( A X. B ) |-> U. `' { x } ) : ( A X. B ) -1-1-onto-> `' ( A X. B ) )
7 4 6 mpbir
 |-  F : ( A X. B ) -1-1-onto-> `' ( A X. B )
8 cnvxp
 |-  `' ( A X. B ) = ( B X. A )
9 f1oeq3
 |-  ( `' ( A X. B ) = ( B X. A ) -> ( F : ( A X. B ) -1-1-onto-> `' ( A X. B ) <-> F : ( A X. B ) -1-1-onto-> ( B X. A ) ) )
10 8 9 ax-mp
 |-  ( F : ( A X. B ) -1-1-onto-> `' ( A X. B ) <-> F : ( A X. B ) -1-1-onto-> ( B X. A ) )
11 7 10 mpbi
 |-  F : ( A X. B ) -1-1-onto-> ( B X. A )