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 )