Suppose $L=\{((a,b),(a',b'))\in(A\times B)\times(A\times B)|aRa' \land(a=a'\rightarrow bSb'\}$. Show that $L$ is a partial order on $A\times B$. Not a duplicate of this, this, or this.
This is exercise $4.4.9$ from the book How to Prove it by Velleman $($$2^{nd}$ edition$)$:
Suppose $R$ is a partial order on $A$ and $S$ is a partial order on $B$. Define a relation $L$ on $A\times B$ as follows: $L=\Bigr\{\bigr((a,b),(a',b')\bigr)\in(A\times B)\times(A\times B)|$
$aRa'\ \text{and if}\ a=a'\ \text{then}\ bSb'\Bigr\}$. Show that $L$ is a partial order on $A\times B$. If both $R$ and $S$ are total orders, will $L$ also be a total order$?$
Here are my answers:
Proof of the first part:
Reflexivity: Let $(a,b)$ be an arbitrary element of $A\times B$ which means $a\in A$ and $b\in B$. Obviously $a=a$. Since $R$ is reflexive $aRa$. Since $S$ is reflexive $bSb$ and so if $a=a$ then $bSb$. Ergo by definition $\bigr((a,b),(a,b)\bigr)\in L$ and since $(a,b)$ is arbitrary, $L$ is reflexive.
Antisymmetry: Let $\bigr((a,b),(a',b')\bigr)$ and $\bigr((a',b'),(a,b)\bigr)$ be arbitrary elements of $L$ This means $aRa'$, $(a=a'\rightarrow bSb')$, $a'Ra$, and $(a=a'\rightarrow b'Sb)$. Since $R$ is antisymmetric, then from $aRa'$ and $a'Ra$ we obtain $a=a'$. Thus by modus ponens we have $bSb'$ and $b'Sb$ and since $S$ is antisymmetric, then $b=b'$. Ergo $(a,b)=(a',b')$. Since $\bigr((a,b),(a',b')\bigr)$ and $\bigr((a',b'),(a,b)\bigr)$ are arbitrary, $L$ is antisymmetric.
Transitivity: Let $(a,b)$, $(a',b')$, and $(a'',b'')$ be arbitrary elements of $A\times B$ such that $\bigr((a,b),(a',b')\bigr)\in L$ which means $aRa'$ and $(a=a'\rightarrow bSb')$ and $\bigr((a',b'),(a'',b'')\bigr)\in L$ which means $a'Ra''$ and $(a'=a''\rightarrow b'Sb'')$. Since $R$ is transitive, $aRa''$. Suppose $a=a''$ and so $a''Ra$. From $a''Ra$ and $aRa'$, $a''Ra'$. From $a''Ra$ and $a'Ra''$, $a'Ra$. Since $R$ is antisymmetric, from $aRa'$ and $a'Ra$ we obtain $a=a'$ and from $a'Ra''$ and $a''Ra'$ we obtain $a'=a''$. Then by modus ponens we have, $bSb'$ and $b'Sb''$ and since $S$ is transitive $bSb''$. Ergo if $a=a''$ then $bSb''$. From $aRa''$ and $(a=a''\rightarrow bSb'')$ by definition we obtain $\bigr((a,b),(a'',b'')\bigr)\in L$. Since $(a,b)$, $(a',b')$, and $(a'',b'')$ are arbitrary, $L$ is transitive.
Since $L$ is reflexive, antisymmetric, and transitive then $L$ is a partial order. $Q.E.D.$
Proof of the second part:
Suppose $R$ and $S$ are total orders. Let $(a,b)$ and $(a',b')$ be arbitrary elements of $A\times B$. This means $a\in A$, $a'\in A$, $b\in B$, and $b'\in B$. We consider four cases.
Case $1.$ Suppose $aRa'$ and $bSb'$. We consider two cases.
Case $1.1.$ Suppose $a=a'$. Ergo $(a,b)L(a',b')$ and so $(a,b)L(a',b')$ or $(a',b')L(a,b)$.
Case $1.2.$ Suppose $a\neq a'$. Ergo $(a,b)L(a',b')$ and so $(a,b)L(a',b')$ or $(a',b')L(a,b)$.
Case $2.$ Suppose $aRa'$ and $b'Sb$. We consider two cases.
Case $2.1.$ Suppose $a=a'$. Ergo $a'Ra$ and so $(a',b')L(a,b)$ which implies $(a,b)L(a',b')$ or $(a',b')L(a,b)$.
Case $2.2.$ Suppose $a\neq a'$. Ergo $(a,b)L(a',b')$ and so $(a,b)L(a',b')$ or $(a',b')L(a,b)$.
Case $3.$ Suppose $a'Ra$ and $bSb'$. We consider two cases.
Case $3.1.$ Suppose $a=a'$. Ergo $aRa'$ and so $(a,b)L(a',b')$ which implies $(a,b)L(a',b')$ or $(a',b')L(a,b)$.
Case $3.2.$ Suppose $a\neq a'$. Ergo $(a',b')L(a,b)$ and so $(a,b)L(a',b')$ or $(a',b')L(a,b)$.
Case $4.$ Suppose $a'Ra$ and $b'Sb$. We consider two cases.
Case $4.1.$ Suppose $a=a'$. Ergo $(a',b')L(a,b)$ and so $(a,b)L(a',b')$ or $(a',b')L(a,b)$.
Case $4.2.$ Suppose $a\neq a'$. Ergo $(a',b')L(a,b)$ and so $(a,b)L(a',b')$ or $(a',b')L(a,b)$.
Since the above cases are exhaustive, $(a,b)L(a',b')$ or $(a',b')L(a,b)$. Since $(a,b)$ and $(a',b')$ are arbitrary, $L$ is a total order. Therefore if $R$ and $S$ are total orders then $L$ is a total order. $Q.E.D.$
Are my proofs valid$?$
Thanks for your attention.
 A: Yes, it’s all correct and perfectly clear; I’ll just make a few comments on what could safely be omitted.
First, it’s never necessary to mention modus ponens by name unless you’re doing some kind of formal logic: it’s just taken for granted. Secondly, most of your ‘which means’ statements could safely be omitted. As an example, I’ll redo the proof of transitivity.

Suppose that $\langle a,b\rangle,\langle a',b'\rangle,\langle a'',b''\rangle\in A\times B$, $\big\langle\langle a,b\rangle,\langle a',b'\rangle\big\rangle\in L$, and $\big\langle\langle a',b'\rangle,\langle a'',b''\rangle\big\rangle\in L$. Then $a\,R\,a'\,R\,a''$, so $a\,R\,a''$, and we automatically have $\langle a,b\rangle\,L\,\langle a'',b''\rangle$ unless $a=a''$. In that case $a''\,R\,a\,R\,a'$, so $a''\,R\,a'\,R\,a''$, and $a'=a''=a$. It follows from the definition of $L$ that $b\,S\,b'\,S\,b''$ and hence that $b\,S\,b''$, and therefore $\langle a,b\rangle\,L\,\langle a'',b''\rangle$ in this case as well, and $L$ is transitive.

In other words, at this point I’m willing to make the reader do a little bit of the work involved in connecting the dots, though all of the critical bits are still there.
For the second part I think that I’d do one case and say that the others are similar, because it really is the same argument each time. And a case can be disposed of a bit more concisely.

Suppose that $a\,R\,a'$ and $b'\,S\,b$. Then either $a\ne a'$ and $\langle a,b\rangle\,L\,\langle a',b'\rangle$, or $a=a'$ and $\langle a',b'\rangle\,L\,\langle a,b\rangle$.

