3 files changed, 105 insertions, 18 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}
diff --git a/library/order/quasiorder.tex b/library/order/quasiorder.tex
index ab325e7..3ccb46e 100644
--- a/library/order/quasiorder.tex
+++ b/library/order/quasiorder.tex
@@ -37,15 +37,48 @@
     Then $a\mathrel{\lt[X]} d$.
 \end{lemma}
 \begin{proof}
-    $\lt[X]$ is transitive.
-    Thus $a\mathrel{\lt[X]} c\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}.
-    Hence $a\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}.
+    $\lt[X]$ is transitive by \cref{quasiorder_tran}.
+    Thus $a\mathrel{\lt[X]} c\mathrel{\lt[X]} d$ by \cref{transitive}.
+    Hence $a\mathrel{\lt[X]} d$ by \cref{transitive}.
+    Follows by assumption.
 \end{proof}
 
 \begin{proposition}\label{subseteqrel_is_quasiorder}
     $\subseteqrel{A}$ is a quasiorder on $A$.
 \end{proposition}
 \begin{proof}
-    $\subseteqrel{A}$ is reflexive on $A$.
-    $\subseteqrel{A}$ is transitive.
+    Show for all $w\in\subseteqrel{A}$ we have $w\in A\times A$.
+    \begin{subproof}
+        Fix $w$.
+        Assume $w\in\subseteqrel{A}$.
+        Take $a,b$ such that $w=(a,b)$ and $a,b\in A$
+            by \cref{subseteqrel,pair_eq_iff}.
+        Follows by \cref{times_tuple_intro}.
+    \end{subproof}
+    Thus $\subseteqrel{A}$ is a binary relation on $A$
+        by \cref{subseteq}.
+    $\subseteqrel{A}$ is reflexive on $A$
+        by \cref{reflexive_on,subseteqrel,subseteq}.
+    Show for all $a,b,c$ such that
+        $a\mathrel{\subseteqrel{A}}b$ and
+        $b\mathrel{\subseteqrel{A}}c$
+        we have $a\mathrel{\subseteqrel{A}}c$.
+    \begin{subproof}
+        Fix $a,b,c$.
+        Assume $a\mathrel{\subseteqrel{A}}b$ and
+            $b\mathrel{\subseteqrel{A}}c$.
+        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$ and $a\in A$ by assumption.
+        Take $u,v$ such that $(b,c)=(u,v)$ and
+            $u,v\in A$ and $u\subseteq v$ by \cref{subseteqrel}.
+        Then $b=u$ and $c=v$ by \cref{pair_eq_iff}.
+        Thus $b\subseteq c$ and $c\in A$ by assumption.
+        Thus $a\subseteq c$ by \cref{subseteq_transitive}.
+        Follows by \cref{subseteqrel}.
+    \end{subproof}
+    Thus $\subseteqrel{A}$ is transitive
+        by \cref{transitive}.
+    Follows by assumption.
 \end{proof}
diff --git a/library/order/semilattice.tex b/library/order/semilattice.tex
index 51af68b..76bbe56 100644
--- a/library/order/semilattice.tex
+++ b/library/order/semilattice.tex
@@ -1,7 +1,8 @@
-\import{order/partial-order.tex}
+\import{order/order.tex}
+\import{function.tex}
 
 \begin{struct}\label{meet_semilattice}
-    A meet semilattice $X$ is a partial order
+    A meet semilattice $X$ is an ordered set
     equipped with
     \begin{enumerate}
         \item $\meet$
@@ -9,7 +10,7 @@
     such that
     \begin{enumerate}
         \item\label{meet_type} for all $x,y\in \carrier[X]$ we have
-           $\meet[X](x,y)\in X$.
+           $\meet[X](x,y)\in \carrier[X]$.
         \item\label{meet_lb} for all $x,y\in \carrier[X]$ we have
             $\meet[X](x,y) \mathrel{\lt[X]} x, y$.
         \item\label{meet_glb} for all $a,x,y\in \carrier[X]$ such that $a\mathrel{\lt[X]} x, y$ we have
@@ -20,12 +21,16 @@
 
 \begin{proposition}\label{meet_idempotent}
     Let $X$ be a meet semilattice.
-    Then $\meet(x,x) = x$.
+    Let $x\in\carrier[X]$.
+    Then $\meet[X](x,x) = x$.
 \end{proposition}
 \begin{proof}
-    $\meet(x,x) \mathrel{\lt} x$.
-    $x\mathrel{\lt[X]} x, x$.
-    Thus $x\mathrel{\lt[X]} \meet(x,x)$.
+    We have $\meet[X](x,x)\in\carrier[X]$ by \cref{meet_type}.
+    We have $\meet[X](x,x)\mathrel{\lt[X]}x$ by \cref{meet_lb}.
+    We have $x\mathrel{\lt[X]}x$
+        by \cref{meet_semilattice,orderedset,quasiorder_refl,reflexive_on}.
+    Thus $x\mathrel{\lt[X]}\meet[X](x,x)$ by \cref{meet_glb}.
+    Follows by \cref{meet_semilattice,orderedset,orderedset_antisym,antisymmetric}.
 \end{proof}
 
 %\begin{proposition}\label{meet_comm}