Migrate base relation proofs to exact checking

Express converse, domain, range, and composition with the checked replacement and separation forms. This preserves their ordered-pair meaning without extending the exact core with the legacy predicate-replacement construct.

1 files changed, 346 insertions, 123 deletions

diff --git a/library/relation.tex b/library/relation.tex
index a93a623..afb99d2 100644
--- a/library/relation.tex
+++ b/library/relation.tex
@@ -19,28 +19,39 @@
     Then $R = S$.
 \end{proposition}
 \begin{proof}
+    We have for all $w\in R$ we have $w\in S$ by \cref{relation}.
+    We have for all $w\in S$ we have $w\in R$ by \cref{relation}.
     Follows by set extensionality.
 \end{proof}
 
 \begin{abbreviation}\label{family_of_relations}
     $F$ is a family of relations iff
-    every element of $F$ is a relation.
+    for all $R\in F$ we have $R$ is a relation.
 \end{abbreviation}
 
 \begin{proposition}\label{unions_of_family_of_relations_is_relation}
     Let $F$ be a family of relations.
     Then $\unions{F}$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,unions_iff}.
+\end{proof}
 
 \begin{proposition}\label{inters_of_family_of_relations_is_relation}
     Let $F$ be a family of relations.
     Then $\inters{F}$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,inters_iff_forall}.
+\end{proof}
 
 \begin{proposition}\label{union_relations_is_relation}
     Let $R, S$ be relations.
     Then $R\union S$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,union_iff}.
+\end{proof}
 
 \begin{proposition}\label{union_relations_is_relation_type}
     Suppose $R\subseteq A\times B$.
@@ -55,41 +66,63 @@
     Let $R, S$ be relations.
     Then $R\inter S$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,inter}.
+\end{proof}
 
 \begin{proposition}\label{setminus_relations_is_relation}
     Let $R, S$ be relations.
     Then $R\setminus S$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,setminus}.
+\end{proof}
 
 
 
 \subsection{Converse of a relation}
 
 \begin{definition}\label{converse_relation}
-    $\converse{R} = \{ z\mid \exists w\in R. \exists x, y. w = (x, y)\land z = (y, x)\}$.
+    $\converse{R} =
+    \{ (\snd{w},\fst{w})\mid w\in R\mid \exists x, y. w = (x, y)\}$.
 \end{definition}
 
 \begin{proposition}\label{converse_intro}
     If $y\mathrel{R} x$, then $x\mathrel{\converse{R}} y$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{converse_relation,fst_eq,snd_eq}.
+\end{proof}
 
 \begin{proposition}\label{converse_elim}
     If $x\mathrel{\converse{R}} y$, then $y\mathrel{R} x$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{converse_relation,pair_eq_iff,fst_eq,snd_eq}.
+\end{proof}
 
 \begin{proposition}\label{converse_iff}
     $x\mathrel{\converse{R}} y$ iff $y\mathrel{R} x$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{converse_intro,converse_elim}.
+\end{proof}
 
 
 \begin{proposition}\label{converse_is_relation}
     $\converse{R}$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,converse_relation}.
+\end{proof}
 
 
 \begin{proposition}\label{converse_converse_iff}
     $x \mathrel{\converse{\converse{R}}} y$ iff $x\mathrel{R} y$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{converse_iff}.
+\end{proof}
 
 % Only works if the starting set was a relation (i.e. only has pairs as elements).
 \begin{proposition}\label{converse_converse_eq}
@@ -97,7 +130,7 @@
     Then $\converse{\converse{R}} = R$.
 \end{proposition}
 \begin{proof}
-    Follows by set extensionality.
+    Follows by \cref{relext,converse_is_relation,converse_converse_iff}.
 \end{proof}
 
 \begin{proposition}\label{converse_type}
@@ -105,29 +138,30 @@
     Then $\converse{R}\subseteq B\times A$.
 \end{proposition}
 \begin{proof}
-    It suffices to show that every element of $\converse{R}$ is an element of $B\times A$
-        by \cref{subseteq}.
-    Fix $w\in\converse{R}$.
-    Take $x, y$ such that $w = (y, x)$ and $x\mathrel{R} y$ by \cref{converse_relation}.
-    Now $(x,y)\in A\times B$ by \cref{subseteq}.
-    Thus $x\in A$ and $y\in B$ by \cref{times_tuple_elim}.
-    Hence $(y,x)\in B\times A$ by \cref{times_tuple_intro}.
+    We have for all $w\in\converse{R}$ we have $w\in B\times A$
+        by \cref{converse_is_relation,relation,converse_iff,subseteq,times_tuple_elim,times_tuple_intro}.
+    Follows by \cref{subseteq}.
 \end{proof}
 
 \begin{proposition}\label{converse_times}
     Then $\converse{B\times A} = A\times B$.
 \end{proposition}
 \begin{proof}
-    For all $w$ we have $w\in\converse{B\times A}$ iff $w\in A\times B$
-        by \cref{converse_relation,times,times_elem_is_tuple,times_tuple_elim}.
-    Follows by \hyperref[setext]{extensionality}.
-    %Follows by set extensionality.
+    We have for all $w\in\converse{B\times A}$ we have $w\in A\times B$
+        by \cref{converse_is_relation,relation,converse_iff,times_elem_is_tuple,times_tuple_elim,times_tuple_intro}.
+    We have for all $w\in A\times B$ we have $w\in\converse{B\times A}$
+        by \cref{converse_iff,times_elem_is_tuple,times_tuple_elim,times_tuple_intro}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{converse_emptyset}
     Then $\converse{\emptyset} = \emptyset$.
 \end{proposition}
 \begin{proof}
+    We have for all $w\in\converse{\emptyset}$ we have $w\in\emptyset$
+        by \cref{converse_relation,emptyset}.
+    We have for all $w\in\emptyset$ we have $w\in\converse{\emptyset}$
+        by \cref{emptyset}.
     Follows by set extensionality.
 \end{proof}
 
@@ -159,32 +193,39 @@
     $\converse{(R\union S)} = \converse{R}\union\converse{S}$.
 \end{proposition}
 \begin{proof}
-    $\converse{(R\union S)}$ is a relation by \cref{converse_is_relation}.
-    $\converse{R}\union\converse{S}$ is a relation by \cref{converse_is_relation,union_relations_is_relation}.
-    For all $a,b$ we have $(a,b)\in\converse{(R\union S)}$ iff $(a,b)\in\converse{R}\union\converse{S}$
-        by \cref{union_iff,converse_iff}.
-    Follows by \hyperref[relext]{extensionality}.
+    We have for all $w\in\converse{(R\union S)}$
+        we have $w\in\converse{R}\union\converse{S}$
+        by \cref{converse_is_relation,relation,union_iff,converse_iff}.
+    We have for all $w\in\converse{R}\union\converse{S}$
+        we have $w\in\converse{(R\union S)}$
+        by \cref{converse_is_relation,union_relations_is_relation,relation,union_iff,converse_iff}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{converse_inter}
     $\converse{(R\inter S)} = \converse{R}\inter\converse{S}$.
 \end{proposition}
 \begin{proof}
-    $\converse{(R\inter S)}$ is a relation by \cref{converse_is_relation}.
-    $\converse{R}\inter\converse{S}$ is a relation by \cref{converse_is_relation,inter_relations_is_relation}.
-    For all $a,b$ we have $(a,b)\in\converse{(R\inter S)}$ iff $(a,b)\in\converse{R}\inter\converse{S}$
-        by \cref{inter,converse_iff}.
-    Follows by \hyperref[relext]{extensionality}.
+    We have for all $w\in\converse{(R\inter S)}$
+        we have $w\in\converse{R}\inter\converse{S}$
+        by \cref{converse_is_relation,relation,inter,converse_iff}.
+    We have for all $w\in\converse{R}\inter\converse{S}$
+        we have $w\in\converse{(R\inter S)}$
+        by \cref{converse_is_relation,inter_relations_is_relation,relation,inter,converse_iff}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{converse_setminus}
     $\converse{(R\setminus S)} = \converse{R}\setminus\converse{S}$.
 \end{proposition}
 \begin{proof}
-    $\converse{(R\setminus S)}$ is a relation by \cref{converse_is_relation}.
-    $\converse{R}\setminus\converse{S}$ is a relation by \cref{converse_is_relation,setminus_relations_is_relation}.
-    For all $a,b$ we have $(a,b)\in\converse{(R\setminus S)}$ iff $(a,b)\in\converse{R}\setminus\converse{S}$.
-    Follows by \hyperref[relext]{extensionality}.
+    We have for all $w\in\converse{(R\setminus S)}$
+        we have $w\in\converse{R}\setminus\converse{S}$
+        by \cref{converse_is_relation,relation,setminus,converse_iff}.
+    We have for all $w\in\converse{R}\setminus\converse{S}$
+        we have $w\in\converse{(R\setminus S)}$
+        by \cref{converse_is_relation,setminus_relations_is_relation,relation,setminus,converse_iff}.
+    Follows by set extensionality.
 \end{proof}
 
 
@@ -192,12 +233,15 @@
 \subsubsection{Domain of a relation}
 
 \begin{definition}\label{dom}
-    $\dom{R} = \{ x\mid \exists w\in R. \exists y. w = (x, y)\}$.
+    $\dom{R} = \{ \fst{w}\mid w\in R\mid \exists x, y. w = (x, y)\}$.
 \end{definition}
 
 \begin{proposition}\label{dom_iff}
     $a\in\dom{R}$ iff there exists $b$ such that $a\mathrel{R} b$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{dom,pair_eq_iff,fst_eq}.
+\end{proof}
 
 \begin{proposition}\label{dom_intro}
     Suppose $a\mathrel{R} b$.
@@ -211,18 +255,29 @@
     $\dom{\emptyset} = \emptyset$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\dom{\emptyset}$ we have $x\in\emptyset$
+        by \cref{dom_iff,emptyset}.
+    We have for all $x\in\emptyset$ we have $x\in\dom{\emptyset}$
+        by \cref{emptyset}.
     Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{dom_times}
     $\dom{(A\times B)}\subseteq A$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,dom_iff,times_tuple_elim}.
+\end{proof}
 
 \begin{proposition}\label{dom_times_inhabited}
     Suppose $b\in B$.
     $\dom{(A\times B)} = A$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\dom{(A\times B)}$ we have $x\in A$
+        by \cref{dom_times,subseteq}.
+    We have for all $x\in A$ we have $x\in\dom{(A\times B)}$
+        by \cref{dom_iff,times_tuple_intro}.
     Follows by set extensionality.
 \end{proof}
 
@@ -230,6 +285,12 @@
     $\dom{\cons{(a,b)}{R}} = \cons{a}{\dom{R}}$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\dom{\cons{(a,b)}{R}}$
+        we have $x\in\cons{a}{\dom{R}}$
+        by \cref{dom_iff,cons_iff,pair_eq_iff}.
+    We have for all $x\in\cons{a}{\dom{R}}$
+        we have $x\in\dom{\cons{(a,b)}{R}}$
+        by \cref{dom_iff,cons_iff,pair_eq_iff}.
     Follows by set extensionality.
 \end{proof}
 
@@ -237,6 +298,12 @@
     $\dom{(A\union B)} = \dom{A}\union\dom{B}$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\dom{(A\union B)}$
+        we have $x\in\dom{A}\union\dom{B}$
+        by \cref{dom_iff,union_iff}.
+    We have for all $x\in\dom{A}\union\dom{B}$
+        we have $x\in\dom{(A\union B)}$
+        by \cref{dom_iff,union_iff}.
     Follows by set extensionality.
 \end{proof}
 
@@ -250,6 +317,9 @@
 \begin{proposition}\label{dom_setminus}
     $\dom{(A\setminus B)}\supseteq \dom{A}\setminus\dom{B}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,setminus,dom_iff}.
+\end{proof}
 
 % TODO (also needs to import set/cons)
 %\begin{proposition}\label{dom_remove_invariant}
@@ -261,12 +331,15 @@
 \subsubsection{Range of a relation}
 
 \begin{definition}\label{ran}
-    $\ran{R} = \{ y\mid \exists w\in R. \exists x. w = (x, y)\}$.
+    $\ran{R} = \{ \snd{w}\mid w\in R\mid \exists x, y. w = (x, y)\}$.
 \end{definition}
 
 \begin{proposition}\label{ran_iff}
     $b\in\ran{R}$ iff there exists $a$ such that $a\mathrel{R} b$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{ran,pair_eq_iff,snd_eq}.
+\end{proof}
 
 \begin{proposition}\label{ran_intro}
     Suppose $a\mathrel{R} b$.
@@ -280,18 +353,29 @@
     $\ran{\emptyset} = \emptyset$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\ran{\emptyset}$ we have $x\in\emptyset$
+        by \cref{ran_iff,emptyset}.
+    We have for all $x\in\emptyset$ we have $x\in\ran{\emptyset}$
+        by \cref{emptyset}.
     Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{ran_times}
     $\ran{(A\times B)}\subseteq B$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,ran_iff,times_tuple_elim}.
+\end{proof}
 
 \begin{proposition}\label{ran_times_inhabited}
     Suppose $a\in A$.
     $\ran{(A\times B)} = B$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\ran{(A\times B)}$ we have $x\in B$
+        by \cref{ran_times,subseteq}.
+    We have for all $x\in B$ we have $x\in\ran{(A\times B)}$
+        by \cref{ran_iff,times_tuple_intro}.
     Follows by set extensionality.
 \end{proof}
 
@@ -299,6 +383,12 @@
     $\ran{(\cons{(a,b)}{R})} = \cons{b}{\ran{R}}$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\ran{\cons{(a,b)}{R}}$
+        we have $x\in\cons{b}{\ran{R}}$
+        by \cref{ran_iff,cons_iff,pair_eq_iff}.
+    We have for all $x\in\cons{b}{\ran{R}}$
+        we have $x\in\ran{\cons{(a,b)}{R}}$
+        by \cref{ran_iff,cons_iff,pair_eq_iff}.
     Follows by set extensionality.
 \end{proof}
 
@@ -306,6 +396,12 @@
     $\ran{(A\union B)} = \ran{A}\union\ran{B}$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\ran{(A\union B)}$
+        we have $x\in\ran{A}\union\ran{B}$
+        by \cref{ran_iff,union_iff}.
+    We have for all $x\in\ran{A}\union\ran{B}$
+        we have $x\in\ran{(A\union B)}$
+        by \cref{ran_iff,union_iff}.
     Follows by set extensionality.
 \end{proof}
 
@@ -329,6 +425,10 @@
     $\dom{\converse{R}} = \ran{R}$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\dom{\converse{R}}$ we have $x\in\ran{R}$
+        by \cref{dom_iff,ran_iff,converse_iff}.
+    We have for all $x\in\ran{R}$ we have $x\in\dom{\converse{R}}$
+        by \cref{dom_iff,ran_iff,converse_iff}.
     Follows by set extensionality.
 \end{proof}
 
@@ -336,6 +436,10 @@
     $\ran{\converse{R}} = \dom{R}$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\ran{\converse{R}}$ we have $x\in\dom{R}$
+        by \cref{dom_iff,ran_iff,converse_iff}.
+    We have for all $x\in\dom{R}$ we have $x\in\ran{\converse{R}}$
+        by \cref{dom_iff,ran_iff,converse_iff}.
     Follows by set extensionality.
 \end{proof}
 
@@ -360,7 +464,7 @@
     Then $a\in\fld{R}$.
 \end{proposition}
 \begin{proof}
-    Follows by \cref{fld,dom,union_iff}.
+    Follows by \cref{fld,dom_iff,union_iff}.
 \end{proof}
 
 \begin{proposition}\label{fld_intro_right}
@@ -368,7 +472,7 @@
     Then $b\in\fld{R}$.
 \end{proposition}
 \begin{proof}
-    Follows by \cref{fld,ran,union_iff}.
+    Follows by \cref{fld,ran_iff,union_iff}.
 \end{proof}
 
 \begin{proposition}\label{dom_subseteq_fld}
@@ -414,43 +518,37 @@
 \begin{proposition}\label{fld_universal}
     $\fld{(A\times A)} = A$.
 \end{proposition}
+\begin{proof}
+    We have for all $x\in\fld{(A\times A)}$ we have $x\in A$
+        by \cref{fld,union_iff,dom_times,ran_times,subseteq}.
+    We have for all $x\in A$ we have $x\in\fld{(A\times A)}$
+        by \cref{fld,union_iff,dom_iff,times_tuple_intro}.
+    Follows by set extensionality.
+\end{proof}
 
 \begin{proposition}\label{fld_emptyset}
     $\fld{\emptyset} = \emptyset$.
 \end{proposition}
+\begin{proof}
+    We have for all $x\in\fld{\emptyset}$ we have $x\in\emptyset$
+        by \cref{fld,union_iff,dom_iff,ran_iff,emptyset}.
+    We have for all $x\in\emptyset$ we have $x\in\fld{\emptyset}$
+        by \cref{emptyset}.
+    Follows by set extensionality.
+\end{proof}
 
 \begin{proposition}\label{fld_cons}
     $\fld{(\cons{(a,b)}{R})} = \cons{a}{\cons{b}{\fld{R}}}$.
 \end{proposition}
 \begin{proof}
-    \begin{align*}
-        \fld{(\cons{(a,b)}{R})}
-        &= \dom{(\cons{(a,b)}{R})}\union\ran{(\cons{(a,b)}{R})}
-            \explanation{by \cref{fld}}\\
-        &= \cons{a}{\dom{R}}\union\cons{b}{\ran{R}}
-            \explanation{by \cref{dom_cons,ran_cons}}\\
-        &= \cons{a}{\cons{b}{\dom{R}\union\ran{R}}}
-            \explanation{by \cref{union_cons,union_comm}}\\
-        &= \cons{a}{\cons{b}{\fld{R}}}
-          \explanation{by \cref{fld}}
-    \end{align*}
+    Follows by \cref{fld,dom_cons,ran_cons,union_cons,union_comm}.
 \end{proof}
 
 \begin{proposition}\label{fld_union}
     $\fld{(A\union B)} = \fld{A}\union\fld{B}$.
 \end{proposition}
 \begin{proof}
-    \begin{align*}
-        \fld{(A\union B)}
-        &= \dom{(A\union B)}\union\ran{(A\union B)}
-            \explanation{by \cref{fld}}\\
-        &= (\dom{A}\union\dom{B})\union(\ran{A}\union\ran{B})
-            \explanation{by \cref{dom_union,ran_union}}\\
-        &= (\dom{A}\union\ran{A})\union(\dom{B}\union\ran{B})
-            \explanation{by \cref{union_comm,union_assoc}}\\
-        &= \fld{A}\union\fld{B}
-        \explanation{by \cref{fld}}
-    \end{align*}
+    Follows by \cref{fld,dom_union,ran_union,union_comm,union_assoc}.
 \end{proof}
 
 \begin{proposition}\label{fld_inter}
@@ -487,12 +585,15 @@
     Then $b\in\img{R}{A}$.
 \end{proposition}
 \begin{proof}
-    Follows by \cref{img,ran}.
+    Follows by \cref{img,ran_iff}.
 \end{proof}
 
 \begin{proposition}\label{img_iff}
     $b\in\img{R}{A}$ iff there exists $a\in A$ such that $a\mathrel{R} b$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{img,ran_iff}.
+\end{proof}
 
 \begin{proposition}\label{img_subseteq}
     Suppose $A\subseteq B$.
@@ -505,16 +606,32 @@
 \begin{proposition}\label{img_subseteq_ran}
     Then $\img{R}{A}\subseteq \ran{R}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,img}.
+\end{proof}
 
 \begin{proposition}\label{img_dom}
     Then $\img{R}{\dom{R}} = \ran{R}$.
 \end{proposition}
+\begin{proof}
+    We have for all $b\in\img{R}{\dom{R}}$ we have $b\in\ran{R}$
+        by \cref{img_subseteq_ran,subseteq}.
+    We have for all $b\in\ran{R}$ we have $b\in\img{R}{\dom{R}}$
+        by \cref{img_iff,dom_iff,ran_iff}.
+    Follows by set extensionality.
+\end{proof}
 
 \begin{proposition}\label{img_union}
     $\img{R}{A\union B} = \img{R}{A}\union\img{R}{B}$.
 \end{proposition}
 \begin{proof}
-    Follows by \cref{setext,union_iff,img_iff}.
+    We have for all $b\in\img{R}{A\union B}$
+        we have $b\in\img{R}{A}\union\img{R}{B}$
+        by \cref{union_iff,img_iff}.
+    We have for all $b\in\img{R}{A}\union\img{R}{B}$
+        we have $b\in\img{R}{A\union B}$
+        by \cref{union_iff,img_iff}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{img_inter}
@@ -536,6 +653,9 @@
 \begin{proposition}\label{img_singleton_iff}
     $b\in \img{R}{\{a\}}$ iff $a\mathrel{R}b$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{img_iff,singleton_iff}.
+\end{proof}
 
 \begin{proposition}\label{img_singleton_intro}
     Suppose $b\in\img{R}{\{a\}}$.
@@ -548,11 +668,18 @@
 \begin{proposition}\label{img_singleton}
     $\img{R}{\{a\}} = \{b\in\ran{R}\mid (a,b)\in R \}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{img,singleton_iff}.
+\end{proof}
 
 \begin{proposition}\label{img_emptyset}
     $\img{R}{\emptyset} = \emptyset$.
 \end{proposition}
 \begin{proof}
+    We have for all $b\in\img{R}{\emptyset}$ we have $b\in\emptyset$
+        by \cref{img_iff,emptyset}.
+    We have for all $b\in\emptyset$ we have $b\in\img{R}{\emptyset}$
+        by \cref{emptyset}.
     Follows by set extensionality.
 \end{proof}
 
@@ -565,11 +692,20 @@
 \begin{proposition}\label{preimg_iff}
     $a\in\preimg{R}{B}$ iff there exists $b\in B$ such that $a\mathrel{R} b$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{preimg,dom_iff}.
+\end{proof}
 
 \begin{proposition}\label{preim_eq_img_of_converse}
     $\preimg{R}{B} = \img{\converse{R}}{B}$.
 \end{proposition}
 \begin{proof}
+    We have for all $a\in\preimg{R}{B}$
+        we have $a\in\img{\converse{R}}{B}$
+        by \cref{preimg_iff,img_iff,converse_iff}.
+    We have for all $a\in\img{\converse{R}}{B}$
+        we have $a\in\preimg{R}{B}$
+        by \cref{preimg_iff,img_iff,converse_iff}.
     Follows by set extensionality.
 \end{proof}
 
@@ -577,15 +713,27 @@
     Suppose $A\subseteq B$.
     Then $\preimg{R}{A}\subseteq \preimg{R}{B}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,preimg_iff}.
+\end{proof}
 
 \begin{proposition}\label{preimg_subseteq_dom}
     Then $\preimg{R}{A}\subseteq \dom{R}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,preimg}.
+\end{proof}
 
 \begin{proposition}\label{preimg_union}
     $\preimg{R}{A\union B} = \preimg{R}{A}\union\preimg{R}{B}$.
 \end{proposition}
 \begin{proof}
+    We have for all $a\in\preimg{R}{A\union B}$
+        we have $a\in\preimg{R}{A}\union\preimg{R}{B}$
+        by \cref{preimg_iff,union_iff}.
+    We have for all $a\in\preimg{R}{A}\union\preimg{R}{B}$
+        we have $a\in\preimg{R}{A\union B}$
+        by \cref{preimg_iff,union_iff}.
     Follows by set extensionality.
 \end{proof}
 
@@ -593,11 +741,17 @@
     % Equality does not hold in general
     $\preimg{R}{A\inter B}\subseteq \preimg{R}{A}\inter\preimg{R}{B}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,preimg_iff,inter}.
+\end{proof}
 
 \begin{proposition}\label{preimg_setminus}
     % Equality does not hold in general
     $\preimg{R}{A\setminus B}\supseteq \preimg{R}{A}\setminus\preimg{R}{B}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,preimg_iff,setminus}.
+\end{proof}
 
 \subsection{Upward and downward closure}
 
@@ -612,6 +766,9 @@
 \begin{proposition}\label{downward_closure_iff}
     $a\in\downward{R}{b}$ iff $a\mathrel{R}b$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{downward_closure,dom_iff}.
+\end{proof}
 
 \subsection{Relation (and later also function) composition}
 
@@ -620,20 +777,24 @@ Note that the order is flipped from usual relation composition.
 This lets us use the same symbol for composition of functions.
 
 \begin{definition}\label{circ}
-    $S\circ R = \{ (x,z)\mid x\in\dom{R}, z\in\ran{S}\mid \exists y.\  x\mathrel{R}y\mathrel{S}z \}$.
+    $S\circ R = \{ w\in\dom{R}\times\ran{S}\mid
+        \exists x, y, z. w = (x,z)\land x\mathrel{R}y\mathrel{S}z \}$.
 \end{definition}
 
 \begin{proposition}\label{circ_is_relation}
     $S\circ R$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,circ}.
+\end{proof}
 
 \begin{proposition}\label{circ_elem_intro}
     Suppose $x\mathrel{R} y\mathrel{S} z$.
     Then $x\mathrel{(S\circ R)} z$.
 \end{proposition}
 \begin{proof}
-    $x\in\dom{R}$ and $z\in\ran{S}$.
-    Then $(x, z)\in S\circ R$ by \cref{circ}.
+    $x\in\dom{R}$ and $z\in\ran{S}$ by \cref{dom_iff,ran_iff}.
+    Then $(x, z)\in S\circ R$ by \cref{circ,times_tuple_intro}.
 \end{proof}
 
 \begin{proposition}\label{circ_elem_elim}
@@ -641,25 +802,21 @@ This lets us use the same symbol for composition of functions.
     Then there exists $y$ such that $x\mathrel{R} y\mathrel{S} z$.
 \end{proposition}
 \begin{proof}
-    %$x\in\dom{R}$ and $z\in\ran{S}$.
-    There exists $y$ such that $x\mathrel{R} y\mathrel{S} z$ by \cref{circ,pair_eq_iff}.
-    Follows by assumption.
+    Follows by \cref{circ,pair_eq_iff}.
 \end{proof}
 
 \begin{proposition}\label{circ_iff}
     $x\mathrel{(S\circ R)} z$ iff there exists $y$ such that $x\mathrel{R} y\mathrel{S} z$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{circ,circ_elem_intro,circ_elem_elim}.
+\end{proof}
 
 \begin{proposition}\label{circ_assoc}
     $(T\circ S)\circ R = T\circ (S\circ R)$.
 \end{proposition}
 \begin{proof}
-    For all $a, b$ we have
-        $(a,b)\in (T\circ S)\circ R$ iff $(a,b)\in T\circ (S\circ R)$
-        by \cref{circ_iff}.
-    Now $(T\circ S)\circ R$ is a relation and $T\circ (S\circ R)$ is a relation by
-        \cref{circ_is_relation}.
-    Follows by \hyperref[relext]{relation extensionality}.
+    Follows by \cref{relext,circ_is_relation,circ_iff}.
 \end{proof}
 
 \begin{proposition}\label{circ_converse_intro_tuple}
@@ -667,10 +824,11 @@ This lets us use the same symbol for composition of functions.
     Then $(a,c)\in \converse{(S\circ R)}$.
 \end{proposition}
 \begin{proof}
-    Take $b$ such that $a\mathrel{\converse{S}} b\mathrel{\converse{R}} c$.
+    Take $b$ such that $a\mathrel{\converse{S}} b\mathrel{\converse{R}} c$
+        by \cref{circ_iff}.
     Now $c\mathrel{R}b\mathrel{S} a$ by \cref{converse_iff}.
-    Hence $c\mathrel{(S\circ R)} a$.
-    Thus $a\mathrel{\converse{(S\circ R)}} c$.
+    Hence $c\mathrel{(S\circ R)} a$ by \cref{circ_iff}.
+    Thus $a\mathrel{\converse{(S\circ R)}} c$ by \cref{converse_iff}.
 \end{proof}
 
 \begin{proposition}\label{circ_converse_elim}
@@ -678,19 +836,17 @@ This lets us use the same symbol for composition of functions.
     Then $(a, c) \in\converse{R}\circ\converse{S}$.
 \end{proposition}
 \begin{proof}
-    $c\mathrel{(S\circ R)} a$.
-    Take $b$ such that  $c\mathrel{R}b\mathrel{S} a$.
-    Now $a\mathrel{\converse{S}} b\mathrel{\converse{R}} c$.
+    $c\mathrel{(S\circ R)} a$ by \cref{converse_iff}.
+    Take $b$ such that $c\mathrel{R}b\mathrel{S} a$ by \cref{circ_iff}.
+    Now $a\mathrel{\converse{S}} b\mathrel{\converse{R}} c$
+        by \cref{converse_iff}.
 \end{proof}
 
 \begin{proposition}\label{circ_converse}
     $\converse{(S\circ R)} = \converse{R}\circ\converse{S}$.
 \end{proposition}
 \begin{proof}
-    $\converse{(S\circ R)}$ is a relation.
-    $\converse{R}\circ\converse{S}$ is a relation.
-    For all $x, y $ we have $(x,y)\in \converse{(S\circ R)}$ iff $(x, y) \in\converse{R}\circ\converse{S}$.
-    Thus $\converse{(S\circ R)} = \converse{R}\circ\converse{S}$ by \cref{relext}.
+    Follows by \cref{relext,converse_is_relation,circ_is_relation,circ_converse_intro_tuple,circ_converse_elim}.
 \end{proof}
 
 \subsection{Restriction}
@@ -703,10 +859,16 @@ This lets us use the same symbol for composition of functions.
 \begin{proposition}\label{restrl_iff}
     $a \mathrel{\restrl{R}{X}} b$ iff $a\mathrel{R}b$ and $a\in X$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{restrl,pair_eq_iff}.
+\end{proof}
 
 \begin{proposition}\label{restrl_subseteq}
     $\restrl{R}{X}\subseteq R$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,restrl}.
+\end{proof}
 
 \begin{proposition}%
 \label{elem_dom_of_restrl_implies_elem_dom_and_restr}
@@ -714,8 +876,10 @@ This lets us use the same symbol for composition of functions.
     Then $x\in \dom{R}, X$.
 \end{proposition}
 \begin{proof}
-    Take $y$ such that $x\in X$ and $(x, y)\in \restrl{R}{X}$.
-    Then $(x, y)\in R$. Thus $x\in\dom{R}$.
+    Take $y$ such that $x\in X$ and $(x, y)\in \restrl{R}{X}$
+        by \cref{dom_iff,restrl_iff}.
+    Then $(x, y)\in R$ by \cref{restrl_iff}.
+    Thus $x\in\dom{R}$ by \cref{dom_iff}.
 \end{proof}
 
 \begin{proposition}%
@@ -725,8 +889,8 @@ This lets us use the same symbol for composition of functions.
 \end{proposition}
 \begin{proof}
     Take $y$ such that $(x, y)\in R$ by \cref{dom_iff}.
-    Then $(x, y)\in \restrl{R}{X}$.
-    Thus $x\in\dom{\restrl{R}{X}}$.
+    Then $(x, y)\in \restrl{R}{X}$ by \cref{restrl_iff}.
+    Thus $x\in\dom{\restrl{R}{X}}$ by \cref{dom_iff}.
 \end{proof}
 
 \begin{proposition}\label{restrl_eq_inter}
@@ -734,9 +898,13 @@ This lets us use the same symbol for composition of functions.
     $\restrl{R}{X} = R\inter (X\times \ran{R})$.
 \end{proposition}
 \begin{proof}
-    For all $a$ we have $a\in R\inter (X\times \ran{R})$ iff $a\in \restrl{R}{X}$
+    We have for all $a\in R\inter (X\times \ran{R})$
+        we have $a\in \restrl{R}{X}$
         by \cref{inter,restrl,ran_iff,times_elem_is_tuple,times_tuple_intro}.
-    Follows by \hyperref[setext]{extensionality}.
+    We have for all $a\in\restrl{R}{X}$
+        we have $a\in R\inter (X\times \ran{R})$
+        by \cref{inter,restrl,ran_iff,times_elem_is_tuple,times_tuple_intro}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{corollary}%
@@ -745,6 +913,12 @@ This lets us use the same symbol for composition of functions.
     $\dom{\restrl{R}{X}} = \dom{R}\inter X$.
 \end{corollary}
 \begin{proof}
+    We have for all $x\in\dom{\restrl{R}{X}}$
+        we have $x\in\dom{R}\inter X$
+        by \cref{elem_dom_of_restrl_implies_elem_dom_and_restr,inter}.
+    We have for all $x\in\dom{R}\inter X$
+        we have $x\in\dom{\restrl{R}{X}}$
+        by \cref{elem_dom_and_restr_implies_elem_of_restr,inter}.
     Follows by set extensionality.
 \end{proof}
 
@@ -753,9 +927,13 @@ This lets us use the same symbol for composition of functions.
     Then $\restrl{\restrl{R}{U}}{V} = \restrl{R}{V}$.
 \end{proposition}
 \begin{proof}
-    For all $w$ we have $w\in\restrl{\restrl{R}{U}}{V}$ iff $w\in\restrl{R}{V}$
+    We have for all $w\in\restrl{\restrl{R}{U}}{V}$
+        we have $w\in\restrl{R}{V}$
+        by \cref{restrl,subseteq}.
+    We have for all $w\in\restrl{R}{V}$
+        we have $w\in\restrl{\restrl{R}{U}}{V}$
         by \cref{restrl,subseteq}.
-    Follows by \hyperref[setext]{extensionality}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{restrl_by_dom}
@@ -763,14 +941,19 @@ This lets us use the same symbol for composition of functions.
     Then $\restrl{R}{\dom{R}} = R$.
 \end{proposition}
 \begin{proof}
-    For all $w$ we have $w\in\restrl{R}{\dom{R}}$ iff $w\in R$
-        by \cref{dom,restrl,relation}.
-    Follows by \hyperref[setext]{extensionality}.
+    We have for all $w\in\restrl{R}{\dom{R}}$ we have $w\in R$
+        by \cref{restrl_subseteq,subseteq}.
+    We have for all $w\in R$ we have $w\in\restrl{R}{\dom{R}}$
+        by \cref{dom_iff,restrl_iff,relation,pair_eq_iff}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{restrl_dom}
     Then $\dom{\restrl{R}{X}}\subseteq X$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,dom_iff,restrl_iff,relation,pair_eq_iff}.
+\end{proof}
 
 \begin{proposition}\label{restrl_ran_elim}
     Suppose $X\subseteq\dom{R}$.
@@ -778,10 +961,7 @@ This lets us use the same symbol for composition of functions.
     Then $b\in\img{R}{X}$.
 \end{proposition}
 \begin{proof}
-    Take $a\in X$ such that $(a, b)\in \restrl{R}{X}$
-        by \cref{dom,ran,restrl_dom,subseteq}.
-    Then $a\mathrel{R} b$ and $b\in\ran{R}$.
-    Thus $b\in\img{R}{X}$ by \cref{img}.
+    Follows by \cref{ran_iff,restrl_iff,img_iff}.
 \end{proof}
 
 \begin{proposition}\label{restrl_ran_intro}
@@ -798,6 +978,10 @@ This lets us use the same symbol for composition of functions.
     Then $\ran{\restrl{R}{X}} = \img{R}{X}$.
 \end{proposition}
 \begin{proof}
+    We have for all $b\in\ran{\restrl{R}{X}}$ we have $b\in\img{R}{X}$
+        by \cref{restrl_ran_elim}.
+    We have for all $b\in\img{R}{X}$ we have $b\in\ran{\restrl{R}{X}}$
+        by \cref{restrl_ran_intro}.
     Follows by set extensionality.
 \end{proof}
 
@@ -806,10 +990,13 @@ This lets us use the same symbol for composition of functions.
     Then $\img{\restrl{R}{X}}{A} = \img{R}{X\inter A}$.
 \end{proposition}
 \begin{proof}
-    For all $b$ we have $b\in\img{\restrl{R}{X}}{A}$ iff $b\in \img{R}{X\inter A}$
+    We have for all $b\in\img{\restrl{R}{X}}{A}$
+        we have $b\in \img{R}{X\inter A}$
         by \cref{restrl_iff,img_iff,inter}.
-    Follows by \hyperref[setext]{extensionality}.
-    %Follows by set extensionality.
+    We have for all $b\in\img{R}{X\inter A}$
+        we have $b\in\img{\restrl{R}{X}}{A}$
+        by \cref{restrl_iff,img_iff,inter}.
+    Follows by set extensionality.
 \end{proof}
 
 
@@ -829,10 +1016,10 @@ This lets us use the same symbol for composition of functions.
     Then $w\in A\times B$.
 \end{proposition}
 \begin{proof}
-    Take $a, b$ such that $(a, b) = w$.
-    Then $a\in\dom{R}$ and $b\in\ran{R}$.
-    Thus $a\in A$ and $b\in B$.
-    Thus $(a, b)\in A\times B$.
+    Take $a, b$ such that $(a, b) = w$ by \cref{relation}.
+    Then $a\in\dom{R}$ and $b\in\ran{R}$ by \cref{dom_iff,ran_iff}.
+    Thus $a\in A$ and $b\in B$ by \cref{subseteq}.
+    Thus $(a, b)\in A\times B$ by \cref{times_tuple_intro}.
 \end{proof}
 
 \begin{proposition}\label{relation_subseteq_intro}
@@ -841,6 +1028,9 @@ This lets us use the same symbol for composition of functions.
     Suppose $\dom{R}\subseteq A$.
     Then $R\subseteq A\times B$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,relation_subseteq_intro_elem}.
+\end{proof}
 
 \begin{proposition}\label{relation_subseteq_implies_dom_subseteq_elem}
     Suppose $R\subseteq A\times B$.
@@ -848,8 +1038,9 @@ This lets us use the same symbol for composition of functions.
     Then $a\in A$.
 \end{proposition}
 \begin{proof}
-    Take $w, b$ such that $w\in R$ and $w = (a, b)$.
-    Follows by \cref{dom,times_tuple_elim,elem_subseteq}.
+    Take $b$ such that $a\mathrel{R}b$ by \cref{dom_iff}.
+    Then $(a,b)\in A\times B$ by \cref{elem_subseteq}.
+    Follows by \cref{times_tuple_elim}.
 \end{proof}
 
 \begin{proposition}\label{relation_subseteq_implies_dom_subseteq}
@@ -866,8 +1057,9 @@ This lets us use the same symbol for composition of functions.
     Then $b\in B$.
 \end{proposition}
 \begin{proof}
-    Take $w, a$ such that $w\in R$ and $w = (a, b)$.
-    Follows by \cref{ran,elem_subseteq,times_tuple_elim}.
+    Take $a$ such that $a\mathrel{R}b$ by \cref{ran_iff}.
+    Then $(a,b)\in A\times B$ by \cref{elem_subseteq}.
+    Follows by \cref{times_tuple_elim}.
 \end{proof}
 
 \begin{proposition}\label{relation_subseteq_implies_ran_subseteq}
@@ -886,6 +1078,10 @@ This lets us use the same symbol for composition of functions.
     Suppose $R\subseteq A\times B$.
     Then $R\in\rels{A}{B}$.
 \end{proposition}
+\begin{proof}
+    Then $R\in\pow{A\times B}$ by \cref{pow_iff,subseteq}.
+    Follows by \cref{rels}.
+\end{proof}
 
 \begin{proposition}\label{rels_intro_dom_and_ran}
     Let $R$ be a relation.
@@ -894,13 +1090,17 @@ This lets us use the same symbol for composition of functions.
     Then $R\in\rels{A}{B}$.
 \end{proposition}
 \begin{proof}
-    $R\subseteq A\times B$.
+    Follows by \cref{relation_subseteq_intro,rels_intro}.
 \end{proof}
 
 \begin{proposition}\label{rels_elim}
     Suppose $R\in\rels{A}{B}$.
     Then $R\subseteq A\times B$.
 \end{proposition}
+\begin{proof}
+    Then $R\in\pow{A\times B}$ by \cref{rels}.
+    Follows by \cref{pow_iff,subseteq}.
+\end{proof}
 
 \begin{proposition}\label{rels_dom_subseteq}
     Suppose $R\in\rels{A}{B}$.
@@ -923,10 +1123,9 @@ This lets us use the same symbol for composition of functions.
     Then $R$ is a relation.
 \end{proposition}
 \begin{proof}
-    It suffices to show that for all $w\in R$ there exists $x, y$ such that $w = (x, y)$.
-    Fix $w\in R$.
-    Now $R\subseteq A\times B$ by \cref{rels_elim}.
-    Thus $w\in A\times B$.
+    We have for all $w\in R$ there exists $x, y$ such that $w = (x, y)$
+        by \cref{rels_elim,subseteq,times_elem_is_tuple}.
+    Follows by \cref{relation}.
 \end{proof}
 
 \begin{proposition}\label{rels_weaken_dom}
@@ -935,8 +1134,8 @@ This lets us use the same symbol for composition of functions.
     Then $R\in\rels{C}{B}$.
 \end{proposition}
 \begin{proof}
-    $R\subseteq A\times B\subseteq C\times B$.
-    Thus $R\subseteq C\times B$.
+    $A\times B\subseteq C\times B$ by \cref{times_subseteq_left}.
+    Follows by \cref{rels_elim,rels_intro,subseteq_transitive}.
 \end{proof}
 
 \begin{proposition}\label{rels_weaken_codom}
@@ -945,8 +1144,8 @@ This lets us use the same symbol for composition of functions.
     Then $R\in\rels{A}{D}$.
 \end{proposition}
 \begin{proof}
-    $R\subseteq A\times B\subseteq A\times D$.
-    Thus $R\subseteq A\times D$.
+    $A\times B\subseteq A\times D$ by \cref{times_subseteq_right}.
+    Follows by \cref{rels_elim,rels_intro,subseteq_transitive}.
 \end{proof}
 
 \begin{proposition}\label{rels_type}
@@ -955,7 +1154,7 @@ This lets us use the same symbol for composition of functions.
     Then $(a,b)\in A\times B$.
 \end{proposition}
 \begin{proof}
-    $R\subseteq A\times B$ by \cref{rels_elim}.
+    Follows by \cref{rels_elim,subseteq}.
 \end{proof}
 
 \begin{proposition}\label{rels_type_dom}
@@ -964,7 +1163,7 @@ This lets us use the same symbol for composition of functions.
     Then $a\in A$.
 \end{proposition}
 \begin{proof}
-    $(a,b)\in A\times B$ by \cref{rels_type}.
+    Follows by \cref{rels_type,times_tuple_elim}.
 \end{proof}
 
 \begin{proposition}\label{rels_type_ran}
@@ -973,7 +1172,7 @@ This lets us use the same symbol for composition of functions.
     Then $b\in B$.
 \end{proposition}
 \begin{proof}
-    $(a,b)\in A\times B$ by \cref{rels_type}.
+    Follows by \cref{rels_type,times_tuple_elim}.
 \end{proof}
 
 \begin{proposition}\label{rels_restrict_dom}
@@ -983,7 +1182,7 @@ This lets us use the same symbol for composition of functions.
 \begin{proof}
     $R$ is a relation by \cref{rels_is_relation}.
     $\dom{R}\subseteq \dom{R}$ by \cref{subseteq_refl}.
-    $\ran{R}\subseteq B$.
+    $\ran{R}\subseteq B$ by \cref{rels_ran_subseteq}.
     Follows by \cref{rels_intro_dom_and_ran}.
 \end{proof}
 
@@ -993,7 +1192,7 @@ This lets us use the same symbol for composition of functions.
 \end{proposition}
 \begin{proof}
     $R$ is a relation by \cref{rels_is_relation}.
-    $\dom{R}\subseteq A$.
+    $\dom{R}\subseteq A$ by \cref{rels_dom_subseteq}.
     $\ran{R}\subseteq \ran{R}$ by \cref{subseteq_refl}.
     Follows by \cref{rels_intro_dom_and_ran}.
 \end{proof}
@@ -1030,35 +1229,50 @@ This lets us use the same symbol for composition of functions.
 \begin{proposition}\label{id_is_relation}
     $\identity{A}$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,id}.
+\end{proof}
 
 \begin{proposition}\label{id_dom}
     $\dom{\identity{A}} = A$.
 \end{proposition}
 \begin{proof}
-    For every $a\in A$ we have $(a, a)\in \identity{A}$.
-    $\dom{\identity{A}} = A$ by set extensionality.
+    We have for all $a\in\dom{\identity{A}}$ we have $a\in A$
+        by \cref{dom_iff,id_iff}.
+    We have for all $a\in A$ we have $a\in\dom{\identity{A}}$
+        by \cref{dom_iff,id_iff}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{id_ran}
     $\ran{\identity{A}} = A$.
 \end{proposition}
 \begin{proof}
-    For every $a$ we have $a\in \ran{\identity{A}}$ iff $a\in A$
+    We have for all $a\in\ran{\identity{A}}$ we have $a\in A$
         by \cref{ran_iff,id_iff}.
-    For every $a\in A$ we have $(a, a)\in \identity{A}$.
-    $\ran{\identity{A}} = A$ by set extensionality.
+    We have for all $a\in A$ we have $a\in\ran{\identity{A}}$
+        by \cref{ran_iff,id_iff}.
+    Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{id_img}
     $\img{\identity{A}}{B} = A\inter B$.
 \end{proposition}
 \begin{proof}
+    We have for all $x\in\img{\identity{A}}{B}$ we have $x\in A\inter B$
+        by \cref{img_iff,id_iff,inter}.
+    We have for all $x\in A\inter B$ we have $x\in\img{\identity{A}}{B}$
+        by \cref{img_iff,id_iff,inter}.
     Follows by set extensionality.
 \end{proof}
 
 \begin{proposition}\label{id_elem_rels}
     $\identity{A}\in\rels{A}{A}$.
 \end{proposition}
+\begin{proof}
+    Follows by
+        \cref{id_is_relation,id_dom,id_ran,subseteq_refl,rels_intro_dom_and_ran}.
+\end{proof}
 
 \subsection{Membership relation}
 
@@ -1071,6 +1285,9 @@ This lets us use the same symbol for composition of functions.
     Suppose $a\in b$.
     Then $(a, b) \in\memrel{A}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{memrel}.
+\end{proof}
 
 \begin{proposition}\label{memrel_elem_inspect}
     Suppose $w\in\memrel{A}$.
@@ -1083,6 +1300,9 @@ This lets us use the same symbol for composition of functions.
 \begin{proposition}\label{memrel_is_relation}
     $\memrel{A}$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,memrel}.
+\end{proof}
 
 \subsection{Subset relation}
 
@@ -1093,3 +1313,6 @@ This lets us use the same symbol for composition of functions.
 \begin{proposition}\label{subseteqrel_is_relation}
     $\subseteqrel{A}$ is a relation.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{relation,subseteqrel}.
+\end{proof}