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

Metamath Proof Explorer

Theorem cnvxp

Description: The converse of a Cartesian product. Exercise 11 of Suppes p. 67. (Contributed by NM, 14-Aug-1999) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion cnvxp 
|- `' ( A X. B ) = ( B X. A )

Proof

Step Hyp Ref Expression
1 cnvopab 
 |-  `' { <. y , x >. | ( y e. A /\ x e. B ) } = { <. x , y >. | ( y e. A /\ x e. B ) }
2 ancom 
 |-  ( ( y e. A /\ x e. B ) <-> ( x e. B /\ y e. A ) )
3 2 opabbii 
 |-  { <. x , y >. | ( y e. A /\ x e. B ) } = { <. x , y >. | ( x e. B /\ y e. A ) }
4 1 3 eqtri 
 |-  `' { <. y , x >. | ( y e. A /\ x e. B ) } = { <. x , y >. | ( x e. B /\ y e. A ) }
5 df-xp 
 |-  ( A X. B ) = { <. y , x >. | ( y e. A /\ x e. B ) }
6 5 cnveqi 
 |-  `' ( A X. B ) = `' { <. y , x >. | ( y e. A /\ x e. B ) }
7 df-xp 
 |-  ( B X. A ) = { <. x , y >. | ( x e. B /\ y e. A ) }
8 4 6 7 3eqtr4i 
 |-  `' ( A X. B ) = ( B X. A )