Metamath Proof Explorer

Definition df-xp

Description: Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. Definition 9.11 of Quine p. 64. For example, ( { 1 , 5 } X. { 2 , 7 } ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } ) ( ex-xp ). Another example is that the set of rational numbers is defined in df-q using the Cartesian product ( ZZ X. NN ) ; the left- and right-hand sides of the Cartesian product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994)

|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }

 |-  A

 |-  B

 |-  ( A X. B )

 |-  x

 |-  y

 |-  x

 |-  x e. A

 |-  y

 |-  y e. B

 |-  ( x e. A /\ y e. B )

 |-  { <. x , y >. | ( x e. A /\ y e. B ) }

 |-  ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }