DEF-CAR. Cartesian Product.
The Cartesian product of $X$ and $Y$ is
\[X\times Y = \{(x,y)\in\mathcal{P}(\mathcal{P}(X\cup Y)):x\in X\land y\in Y\}.\]Notice that, because in general $((x,y),z)\neq (x,(y,z))$ for arbitrary $x$, $y$ and $z$, $\times$ is technically not associative. Nevertheless, we define
\[\begin{align*} X\times Y\times Z &= (X\times Y)\times Z, \\ X\times Y\times Z\times U &= (X\times Y\times Z)\times U, \end{align*}\]and so on.
If $n\in\mathbb{N}^+$, we write
\[X^n = \underbrace{X\times\cdots\times X}_{\text{$n$ times}}.\]
PROP-CAR-EMP.
For any $X$,
\[X\times\varnothing = \varnothing\times X = \varnothing.\]
PROP-CAR-ITSC.
For any $A$, $B$, $C$ and $D$,
\[(A\cap B)\times(C\cap D) = (A\times C)\cap(B\times D).\]
PROP-CAR-DIST.
For any $A$, $B$ and $C$:
- $A\times(B\cap C) = (A\times B)\cap(A\times C)$.
- $A\times(B\cup C) = (A\times B)\cup(A\times C)$.
- $A\times(B\smallsetminus C) = (A\times B)\smallsetminus(A\times C)$.