Prove $A\times B\subseteq X\times Y\Longleftrightarrow(A\subseteq X)\land(B\subseteq Y)$ I am self-studying through Amann & Escher, Analysis, Vol 1, Chapter 1. I created the following proof and wonder if I have succeeded. If I have (I feel that I have with the caveat that I wonder if I made too big of a leap possibly on one of the steps - I am so new at this that I don't have a sense of correctness or style yet firmly developed), then I'll give an answer credit to anyone who helps me improve the proof or otherwise learn something to make it more robust. If it is not yet a correct proof, then I'll award an answer to the individual who can point out why and a hint as to what I must do to make it satisfactory.
7) Let $X$ and $A$ be subsets of a set $U$ and let $Y$ and $B$
be subsets of a set V. Prove the following:
a) If $A\times B\ne\emptyset$, then $A\times B\subseteq X\times Y\Longleftrightarrow(A\subseteq X)\land(B\subseteq Y).$
We must show that $A\times B\subseteq X\times Y\Longrightarrow(A\subseteq X)\wedge(B\subseteq Y)$
and that $(A\subseteq X)\land(B\subseteq Y)\Longrightarrow A\times B\subseteq X\times Y.$
Proof.
``$\Longrightarrow$'':
This part of the proof is done by contradiction. Suppose $A\times B\subseteq X\times Y$
and $\lnot[(A\subseteq X)\land(B\subseteq Y)]$. $A\times B\subseteq X\times Y$
means that for all $a$ and for all $b$, if $(a,b)\in A\times B$
then $(a,b)\in X\times Y$. $\lnot[(A\subseteq X)\land(B\subseteq Y)]$
means that for some $a\in A,a\notin X$ or for some $b\in B,b\notin Y$.
From this last sentence we deduce that there exists some pair $(a,b)\in A\times B$
such that $(a,b)\notin X\times Y$. But that contradicts our premise:
$A\times B\subseteq X\times Y.$ Therefore, $\lnot[(A\subseteq X)\land(B\subseteq Y)]$
must be false and $(A\subseteq X)\land(B\subseteq Y)$ must be true.
Hence, we have shown that $A\times B\subseteq X\times Y\Longrightarrow(A\subseteq X)\land(B\subseteq Y).$
``$\Longleftarrow$'':
This part of the proof is done by contradiction. Suppose $(A\subseteq X)\land(B\subseteq Y)$
and that the statement $A\times B\subseteq X\times Y$ is false. $(A\times B\not\subseteq X\times Y)$
means there is some $(a,b)\in A\times B$ such that $(a,b)\notin X\times Y$.
From this we deduce that for some $a\in A,a\notin X$ and for some
$b\in B,b\notin Y$. But that contradicts our premise: $(A\subseteq X)\land(B\subseteq Y)$.
Therefore, $\lnot(A\times B\subseteq X\times Y)$ must be false and
$A\times B\subseteq X\times Y$ must be true. Hence, we have shown
that $(A\subseteq X)\land(B\subseteq Y)\Longrightarrow A\times B\subseteq X\times Y$.
Thus, the statement ``if $A\times B\ne\emptyset$, then $A\times B\subseteq X\times Y\Longleftrightarrow(A\subseteq X)\land(B\subseteq Y)$''
must be true.
 A: *

*$\left (A \subseteq X\right) \land  \left (B \subseteq Y\right)\implies \left(A\times B\right) \subseteq  \left(X\times Y\right)$ 

*$\left(A\times B\right) \subseteq  \left(X\times Y\right) \implies (a,b)\in \left(X\times Y\right) \left(a\in A \land b \in B\right) \implies a\in X \land b\in Y \implies A\subseteq X \land B \subseteq Y$
A: $
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\calcop}[2]{\\ #1 \quad & \quad \unicode{x201c}\text{#2}\unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}
$Just for fun, here is an alternative style of proof: start at the most complex side, expand the definitions, apply the laws of logic, simplify, and see where that leads.
It looks like the left hand side is the most complex one, and therefore we calculate as follows:
$$\calc
A \times B \;\subseteq\; X \times Y
\calcop\equiv{definition of $\;\subseteq\;$; definition of $\;\times\;$, twice}
\langle \forall a,b : a \in A \land b \in B : a \in X \land b \in Y \rangle
\calcop\equiv{logic: $\;\forall\;$ distributes over $\;\land\;$ -- there isn't much else we can do}
\langle \forall a,b : a \in A \land b \in B : a \in X \rangle
\;\land\;
\langle \forall a,b : a \in A \land b \in B : b \in Y \rangle
\calcop\equiv{logic: separate the quantifications, twice -- to separate $\;a\;$ from $\;b\;$}
\langle \forall b : b \in B : \langle \forall a : a \in A : a \in X \rangle \rangle
\;\land\;
\langle \forall a : a \in A : \langle \forall b : b \in B : b \in Y \rangle \rangle
\calcop\equiv{logic: write $\;P \Rightarrow Q\;$ as $\;\lnot P \lor Q\;$ and extract $\;{} \lor Q\;$ out of $\;\forall\;$, twice}
(\langle \forall b :: b \not\in B \rangle \lor \langle \forall a : a \in A : a \in X \rangle)
\;\land\;
(\langle \forall a :: a \not\in A \rangle \lor \langle \forall b : b \in B : b \in Y \rangle)
\calcop\equiv{definitions of $\;\emptyset\;$ and $\;\subseteq\;$, both twice}
(B = \emptyset \lor A \subseteq X) \;\land\; (A = \emptyset \lor B \subseteq Y)
\endcalc$$
And if we're given that $\;A,B\;$ are both non-empty, then that last line simplifies to $\;A \subseteq X \;\land\; B \subseteq Y\;$, so that we've proven
$$
A \times B \;\subseteq\; X \times Y \;\equiv\; A \subseteq X \;\land\; B \subseteq Y
$$
as required.
