Trichotomy proof in elementary set theory of relations. I am working through problems in elementary relation theory in an Elias Zakon textbook and would like to ask for your feedback about robustness of my proof. Improvement suggestions are very much welcome.
Problem: 
$\text{Let } R \text{ be a relation with } D_R = D_R^{'} = A$
$R \text{ is trichotomic on } A \text{ if } R \cap R^{-1} = \emptyset = R \cap I_A \text{ and } A \times A  \subseteq R \cup R^{-1} \cup I_A$
Where: 
$D_R \text{ is } R$'s domain. $D_R^{'} \text{ is } R$'s codomain.
$I_A = \{ (x,x) \mid x \in A \}$
$R^{-1}$ is the inverse relation of $R$.
Trichotomy is defined as thus: 
$R \text{ is trichotomic on } A \text{ iff for any } x \text{ and } y \in A \text{ we always have either } xRy, \text{ or } yRx, \text{ or } x = y, \text{ but never two of these together. }$
Proof:
$A \times A  \subseteq R \cup R^{-1} \cup I_A$ is given, so $R \cup R^{-1} \cup I_A$ contains all $(x,y), x \in A, y \in A$.
$R \cap I_A = \emptyset$ is given, so there are no $(x,x)$ $x \in A$ in $R$ and by definition not in $R^{-1}$ either.
Let $D = R \cup R^{-1} \cup I_A - I_A$. By definition of set difference, $D$ contains all $(x,y), x \in A, y \in A$ that are in $R \cup R^{-1} \cup I_A$ but not in $I_A$.
Since it is established that $R \cap I_A = \emptyset$ and $R^{-1} \cap I_A = \emptyset$ hence $D = R \cup R^{-1}$.
It is given that $R \cap R^{-1} = \emptyset$ hence for all $(x,y) \in R \cup R^{-1} \text{ and } x \neq y$ that are in $R$ $(y,x)$ does not also hold in $R$. For all $(x,y) \in R \cup R^{-1} \text{ and } x \neq y$ that are not in $R$ but are in $R^{-1}$ $(y,x)$ does hold in $R$.
Futhermore, it is established that $(x,x)$ does not hold in $R$ for each $x \in A$ hence only $x = x$ is satisfied.
So for all $(x,y)$ $x \in A, y \in A$ only one of $(x,y)$ or $(y,x)$ holds in $R$ or $x = y$. 
$R$ is trichotomic on A. $\blacksquare$
 A: I'm a bit hesitant to add this answer, since it doesn't directly answer your question, but instead shows a proof in a different style.  However, it may help you get a different perspective on the problem and how to approach it.$%
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\brk}{ \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{Ref}[1]{\text{(#1)}}
\newcommand{\then}{\Rightarrow}
\newcommand{\when}{\Leftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
\newcommand{\oneof}[1]{\text{exactly one of }#1\text{ holds}}
%$
Given a set $\;A\;$ and a relation $\;R\;$ on $\;A\;$, and definition
$$
\tag{0}
R \text{ is trichotomic on } A \\\equiv\; \langle \forall x,y : x,y \in A : \oneof{xRy,\; yRx,\; x=y} \rangle
$$
you are asked to prove
$$
\tag{1}
R \text{ is trichotomic on } A \\\when\; R \cap R^{-1} = \emptyset \;\land\; R \cap I_A = \emptyset \;\land\; A \times A  \subseteq R \cup R^{-1} \cup I_A
$$
Comparing the right hand sides of $\Ref{0}$ and $\Ref{1}$, it seems difficult to work from the latter to the former.  Therefore we start at the former, and try to introduce $\;R^{-1}\;$, $\;I_A\;$, and $\;A \times A\;$.

Therefore we start to calculate as follows:
$$\calc
    \langle \forall x,y : x,y \in A : \oneof{xRy,\; yRx,\; x=y} \rangle
\op\equiv\hint{introduce $\;A \times A,\; R^{-1},\; I_A\;$; rewrite $\;xRy\;$ for symmetry}
    \langle \forall x,y : (x,y) \in A \times A : \brk \oneof{(x,y) \in R,\; (x,y) \in R^{-1},\; (x,y) \in I_A} \rangle
\endcalc$$
Now we recognize that this statement really describes a partitioning of $\;A \times A\;$, and that the right hand side of $\Ref{1}$ also seems to be about that same concept.
Therefore we continue the above calculation:
$$\calc
    \dots
\op\equiv\hints{element-level definition of $\;\text{partitions}\;$}\hint{-- to get rid of the individual elements $\;x,y\;$}
    \tag{*} \left\{R, R^{-1}, I_A\right\} \text{ partitions } A \times A
\op\equiv\hint{set-level definition of $\;\text{partitions}\;$}
    R \cap R^{-1} = \emptyset \;\land\; R \cap I_A = \emptyset \;\land\; R^{-1} \cap I_A = \emptyset
    \brk\land\;
    R \cup R^{-1} \cup I_A = A \times A
\endcalc$$
When now comparing this last expression with the right hand side of $\Ref{1}$, we see that there are two differences that we need to focus on: $\;R^{-1} \cap I_A = \emptyset\;$ and $\;R \cup R^{-1} \cup I_A \;\subseteq\; A \times A\;$.  
For the first of these, the only thing I see is to try and use the definitions, in other words, calculate which pairs are in $\;R^{-1} \cap I_A\;$: for every $\;x,y\;$,
$$\calc    
    (x,y) \in R^{-1} \cap I_A
\op\equiv\hint{definition of $\;\cap\;$}
    (x,y) \in R^{-1} \;\land\; (x,y) \in I_A
\op\equiv\hint{definition of $\;I_{\dots}\;$}
    (y,x) \in R \;\land\; x=y
\op\equiv\hint{definition of $\;I_{\dots}\;$}
    (y,x) \in R \;\land\; (y,x) \in I_A
\op\equiv\hint{definition of $\;\cap\;$}
    (y,x) \in R \cap I_A
\endcalc$$
and it immediately follows that $\;R^{-1} \cap I_A = \emptyset \;\equiv\; R \cap I_A = \emptyset\;$.
For the second difference, we calculate simply
$$\calc
    R \cup R^{-1} \cup I_A \;\subseteq\; A \times A
\op\equiv\hint{set theory}
    R \subseteq A \times A \;\land\; R^{-1} \subseteq A \times A \;\land\; I_A \subseteq A \times A
\op\equiv\hint{use twice that $\;R\;$ is a relation on $\;A\;$; definition of $\;I_{\dots}\;$}
    \true
\endcalc$$
With those we can conclude the main calculation:
$$\calc
    \dots
\op\equiv\hint{logic and set theory, by the previous two calculations}
    R \cap R^{-1} = \emptyset \;\land\; R \cap I_A = \emptyset
    \;\land\;
    A \times A \;\subseteq\;R \cup R^{-1} \cup I_A
\endcalc$$
which completes the proof that the right hand sides of $\Ref{0}$ and $\Ref{1}$ are equivalent.

Looking over the above proof, we now see that the key to this problem is that $\;A \times A\;$ is partitioned by $\;R\;$, $\;R^{-1}\;$, and $\;I_A\;$, and that that concept of partitioning can be expressed in two different ways: $\Ref{0}$ expresses it at the level of elements ($\;\oneof{\dots}\;$), and $\Ref{1}$ at the level of sets (empty intersections, union is all).
