Is this proof of $X\times Y=\emptyset\iff X=\emptyset \lor Y=\emptyset$ rigorous enough wrt predicate logic?

Question

I've seen a similar question, but this question is concerned with my proof.

Here is my proof.

$\Rightarrow$) Assume $X\neq\emptyset\land Y\neq\emptyset$.

$X\neq\emptyset\land Y\neq\emptyset\Rightarrow\exists x\colon x\in X\land \exists y\colon y\in Y \Rightarrow x_0\in X\land y_0\in Y\Rightarrow (x_0,y_0)\in X\times Y\Rightarrow X\times Y\neq\emptyset$.

Thus, we have a contradiction.

$\Leftarrow$)

$X\times Y\neq \emptyset\Rightarrow\exists s\colon s\in X\times Y\Rightarrow s_0\in X\times Y\Rightarrow\exists x\exists y\colon x\in X\land y\in Y\land s_0=(x,y)\Rightarrow x_0\in X\land y_0\in Y\land s_0 = (x_0,y_0)\Rightarrow X\neq\emptyset\land Y\neq\emptyset$

Are all the steps in the proof justified? There may be subtle moments not stated explicitly I might have missed. I want to make the proof as rigorous as possible, so if some implications require additional argumentation, could you point that out and explain?

P.S. Yes, I'm a little meticulous. Sorry for that.

Answer 1

You could have done this proof differently: $ X \times Y=\emptyset \iff \forall x,y; (x,y) \notin X \times Y \iff x\notin X \lor y\notin Y (\forall x,y) \iff X=\emptyset \lor Y=\emptyset$ $X \times Y$ is defined as $\{(x,y) \vert x \in X \land y \in Y \}$ therefore it is impossible for an element of $X \times Y$ not to be a pair.