1 files changed, 55 insertions, 6 deletions

diff --git a/library/order/order.tex b/library/order/order.tex
index 1b7692f..dc9497c 100644
--- a/library/order/order.tex
+++ b/library/order/order.tex
@@ -45,13 +45,16 @@
 \begin{proposition}\label{toorder_reflexive}
     $\toorder{A}{R}$ is reflexive on $A$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{toorder,reflexive_on,id_iff,union_iff}.
+\end{proof}
 
 \begin{proposition}\label{toorder_intro}
     Suppose $(a,b)\in R$.
     Then $(a,b)\in\toorder{A}{R}$.
 \end{proposition}
 \begin{proof}
-    $R\subseteq\toorder{A}{R}$.
+    Follows by \cref{toorder,union_iff}.
 \end{proof}
 
 \begin{proposition}\label{toorder_elim}
@@ -65,14 +68,33 @@
 \begin{proposition}\label{toorder_iff}
     $(a,b)\in\toorder{A}{R}$ iff $(a,b)\in R$ or $a = b\in A$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{toorder,id_iff,union_iff}.
+\end{proof}
 
 \begin{proposition}\label{strictorder_from_order}
     Suppose $R$ is an order.
     Then $\tostrictorder{R}$ is a strict order.
 \end{proposition}
 \begin{proof}
-    $\tostrictorder{R}$ is asymmetric.
-    $\tostrictorder{R}$ is transitive.
+    $\tostrictorder{R}$ is asymmetric
+        by \cref{antisymmetric,asymmetric,tostrictorder_iff}.
+    Show for all $a,b,c$ such that
+        $a\mathrel{\tostrictorder{R}}b$ and
+        $b\mathrel{\tostrictorder{R}}c$
+        we have $a\mathrel{\tostrictorder{R}}c$.
+    \begin{subproof}
+        Fix $a,b,c$.
+        Assume $a\mathrel{\tostrictorder{R}}b$ and
+            $b\mathrel{\tostrictorder{R}}c$.
+        We have $a\mathrel{R}b$ and $b\mathrel{R}c$
+            by \cref{tostrictorder_iff}.
+        Thus $a\mathrel{R}c$ by \cref{transitive}.
+        We have $a\neq c$ by \cref{asymmetric}.
+        Follows by \cref{tostrictorder_iff}.
+    \end{subproof}
+    Thus $\tostrictorder{R}$ is transitive by \cref{transitive}.
+    Follows by assumption.
 \end{proof}
 
 \begin{proposition}\label{order_from_strictorder}
@@ -81,16 +103,42 @@
     Then $\toorder{A}{R}$ is an order on $A$.
 \end{proposition}
 \begin{proof}
-    $\toorder{A}{R}$ is antisymmetric.
+    $\identity{A}\subseteq A\times A$
+        by \cref{id_elem_rels,rels_elim}.
+    Thus $\toorder{A}{R}\subseteq A\times A$
+        by \cref{toorder,union_subsets_is_subset}.
+    Hence $\toorder{A}{R}$ is a binary relation on $A$
+        by assumption.
+    $\toorder{A}{R}$ is antisymmetric
+        by \cref{antisymmetric,asymmetric,toorder_iff}.
     $\toorder{A}{R}$ is transitive by \cref{transitive,toorder_iff}.
-    $\toorder{A}{R}$ is reflexive on $A$.
+    $\toorder{A}{R}$ is reflexive on $A$ by \cref{toorder_reflexive}.
+    Follows by assumption.
 \end{proof}
 
 \begin{proposition}\label{subseteqrel_antisymmetric}
     $\subseteqrel{A}$ is antisymmetric.
 \end{proposition}
 \begin{proof}
-    Follows by \cref{subseteqrel,antisymmetric,pair_eq_iff,subseteq_antisymmetric}.
+    Show for all $a,b$ such that
+        $a\mathrel{\subseteqrel{A}}b$ and
+        $b\mathrel{\subseteqrel{A}}a$
+        we have $a=b$.
+    \begin{subproof}
+        Fix $a,b$.
+        Assume $a\mathrel{\subseteqrel{A}}b$ and
+            $b\mathrel{\subseteqrel{A}}a$.
+        Take $x,y$ such that $(a,b)=(x,y)$ and
+            $x,y\in A$ and $x\subseteq y$ by \cref{subseteqrel}.
+        Then $a=x$ and $b=y$ by \cref{pair_eq_iff}.
+        Thus $a\subseteq b$ by assumption.
+        Take $u,v$ such that $(b,a)=(u,v)$ and
+            $u,v\in A$ and $u\subseteq v$ by \cref{subseteqrel}.
+        Then $b=u$ and $a=v$ by \cref{pair_eq_iff}.
+        Thus $b\subseteq a$ by assumption.
+        Follows by \cref{subseteq_antisymmetric}.
+    \end{subproof}
+    Follows by \cref{antisymmetric}.
 \end{proof}
 
 
@@ -100,4 +148,5 @@
 \begin{proof}
     $\subseteqrel{A}$ is a quasiorder on $A$ by \cref{subseteqrel_is_quasiorder}.
     $\subseteqrel{A}$ is antisymmetric by \cref{subseteqrel_antisymmetric}.
+    Follows by assumption.
 \end{proof}