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 ) |