Proving that for any sets $A,B,C$, and $D$, if $(A\times B)\cap (C\times D)=\emptyset $, then $A \cap C = \emptyset $ or $B \cap D = \emptyset $ I'm trying to prove that for any sets $A$, $B$, $C$, and $D$, if the Cartesian product of $A$ and $B$ is disjoint with the Cartesian product of $C$ and $D$, then either $A$ and $C$ are disjoint or $B$ and $D$ are disjoint:
$(A \times B \cap C \times D = \emptyset) \to (A \cap C = \emptyset \lor B \cap D = \emptyset)$
I've tried proving by direct proof by assuming the left side, but I don't know how to deal with the equals sign and the $\emptyset$. I also tried defining disjoint as an implication itself, so that the left side is this:
$(x, y) \in A \times B \to (x, y) \not\in C\times D$
But then when assuming the left side, I don't know how to deal with the $\to$. I was only able to get this far:
$x \in A \land y \in B \to x \not\in C \lor y \not\in D$
Any ideas on how to prove this?
 A: Let $A\cap C\neq\emptyset$ and $B\cap D\neq\emptyset$. So $$\exists x\in A\cap C,~~\exists y\in B\cap D $$ So $$(x,y)\in A\times B,~~(x,y)\in C\times D$$ But 
 $$ (A\times B)\cap(C\times D)=\emptyset$$ This is a pretty contradiction!.
A: A proof with contradiction might work. Assume that $(A \times B) \cap (C \times D) = \emptyset$ such that $A \cap C \ne\emptyset$ and $B \cap D \ne \emptyset$ then you can pick $x \in A \cap C$ and $y \in B \cap D$ but then you will have $(x,y) \in A \times B$ and $(x,y) \in C \times D$ which implies that $(x,y) \in (A \times B) \cap (C \times D)$ which is a contradiction.
A: Here is a proof that may add some insight that is not in any of the previous answers.  Some people will find this too formal, but I find the formalism actually makes it easy to design proofs like this: for many steps there is only one useful thing to do.
I'll use the following definition of cartesian product $\times$: $$
p \in V \times W \;\;\equiv\;\; \textrm{ispair}(p) \land \textrm{fst}(p) \in V \land \textrm{snd}(p) \in W
$$
The most complex expression in the question is the set $(A \times B) \cap (C \times D)$, and since in my experience it helps to reduce set theory questions to the logic level, we will calculate which elements are in this set: for all $p$
$$
\begin{align}
& p \in (A \times B) \cap (C \times D) \\
\equiv & \;\;\;\;\;\text{"definition of $\cap$"} \\
& p \in A \times B \;\;\land\;\; p \in C \times D \\
\equiv & \;\;\;\;\;\text{"the above definition of $\times$, twice"} \\
& \textrm{ispair}(p) \land \textrm{fst}(p) \in A \land \textrm{snd}(p) \in B \;\;\land\;\; \textrm{ispair}(p) \land \textrm{fst}(p) \in C \land \textrm{snd}(p) \in D \\
\equiv & \;\;\;\;\;\text{"logic: rearrange -- this seems the only useful thing we can do now"} \\
& \textrm{ispair}(p) \;\;\land\;\; \textrm{fst}(p) \in A \land \textrm{fst}(p) \in C \;\;\land\;\; \textrm{snd}(p) \in B \land \textrm{snd}(p) \in D \\
\equiv & \;\;\;\;\;\text{"reintroduce $\cap$ using definition, twice -- brings $A$, $C$ together, and $B$, $D$"} \\
& \textrm{ispair}(p) \;\;\land\;\; \textrm{fst}(p) \in A \cap C \;\;\land\;\; \textrm{snd}(p) \in B \cap D \\
\equiv & \;\;\;\;\;\textrm{"reintroduce $\times$ using its definition"} \\
& p \in (A \cap C) \times (B \cap D) \\
\end{align}
$$
Therefore by extensionality, $$
(0) \;\; (A \times B) \cap (C \times D) \;=\; (A \cap C) \times (B \cap D)
$$ and our remaining proof obligation is $$
(1) \;\; (A \cap C) \times (B \cap D) = \emptyset \;\to\; A \cap C = \emptyset \;\lor\; B \cap D = \emptyset
$$  The shape of this statement suggests that we investigate the more general statement $V \times W = \emptyset$:
$$
\begin{align}
& V \times W = \emptyset \\
\equiv & \;\;\;\;\;\text{"property of $\emptyset$"} \\ 
& \langle \forall p :: \lnot(p \in V \times W) \rangle \\
\equiv & \;\;\;\;\;\text{"definition of $\times$ -- this seems the only way to make progress"} \\ 
& \langle \forall p :: \lnot(\textrm{ispair}(p) \land \textrm{fst}(p) \in V \land \textrm{snd}(p) \in W) \rangle \\
\equiv & \;\;\;\;\;\text{"logic: rearrange using DeMorgan"} \\ 
& \langle \forall p : \textrm{ispair}(p) : \lnot(\textrm{fst}(p) \in V) \lor \lnot(\textrm{snd}(p) \in W) \rangle \\
\equiv & \;\;\;\;\;\text{"different way of quantifying over pairs"} \\ 
& \langle \forall v,w :: \lnot(v \in V) \lor \lnot(w \in W) \rangle \\
\equiv & \;\;\;\;\;\text{"logic: split quantification"} \\ 
& \langle \forall v :: \lnot(v \in V) \rangle \lor \langle \forall w :: \lnot(w \in W) \rangle \\
\equiv & \;\;\;\;\;\text{"property of $\emptyset$, twice"} \\ 
& V = \emptyset \;\lor\; W = \emptyset \\
\end{align}
$$
This proves the following generalization of (1): $$
(2) \;\; V \times W = \emptyset \;\equiv\; V = \emptyset \;\lor\; W = \emptyset
$$ So putting all together we've proved $$
(A \times B) \cap (C \times D) = \emptyset \;\equiv\; A \cap C = \emptyset \;\lor\; B \cap D = \emptyset
$$ And en passant we discovered useful theorems (0) and (2).
A: You can prove instead that
$$(A \times B \cap C \times D = \emptyset \,;\, A \cap C \neq \emptyset) \to (B \cap D = \emptyset)$$
Let $x \in A \cap C$. Let $y \in B$, then $(x,y) \in A \times B \Rightarrow (x,y) \notin C \times D \Rightarrow y \notin D$.
This is not really different than the proofs by contradiction posted above though...
