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 A × B x -1
Assertion xpcomf1o F : A × B 1-1 onto B × A

Proof

Step Hyp Ref Expression
1 xpcomf1o.1 F = x A × B x -1
2 relxp Rel A × B
3 cnvf1o Rel A × B x A × B x -1 : A × B 1-1 onto A × B -1
4 2 3 ax-mp x A × B x -1 : A × B 1-1 onto A × B -1
5 f1oeq1 F = x A × B x -1 F : A × B 1-1 onto A × B -1 x A × B x -1 : A × B 1-1 onto A × B -1
6 1 5 ax-mp F : A × B 1-1 onto A × B -1 x A × B x -1 : A × B 1-1 onto A × B -1
7 4 6 mpbir F : A × B 1-1 onto A × B -1
8 cnvxp A × B -1 = B × A
9 f1oeq3 A × B -1 = B × A F : A × B 1-1 onto A × B -1 F : A × B 1-1 onto B × A
10 8 9 ax-mp F : A × B 1-1 onto A × B -1 F : A × B 1-1 onto B × A
11 7 10 mpbi F : A × B 1-1 onto B × A