\import{set.tex}
\import{set/powerset.tex}
\import{set/product.tex}

\section{Relations}

\begin{definition}\label{relation}
    $R$ is a relation iff
    for all $w\in R$ there exists $x, y$ such that $w = (x, y)$.
\end{definition}

\begin{definition}\label{comparable}
    $a$ is comparable with $b$ in $R$ iff $a\mathrel{R}b$ or $b\mathrel{R}a$.
\end{definition}

\begin{proposition}\label{relext}
    Let $R, S$ be relations.
    Suppose for all $x,y$ we have $x\mathrel{R} y$ iff $x\mathrel{S} y$.
    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
    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$.
    Suppose $S\subseteq C\times D$.
    Then $R\union S\subseteq (A\union C)\times (B\union D)$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq,union_times_elim,union_iff,union_subseteq_union}.
\end{proof}

\begin{proposition}\label{inter_relations_is_relation}
    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} =
    \{ (\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}
    Let $R$ be a relation.
    Then $\converse{\converse{R}} = R$.
\end{proposition}
\begin{proof}
    Follows by \cref{relext,converse_is_relation,converse_converse_iff}.
\end{proof}

\begin{proposition}\label{converse_type}
    Suppose $R\subseteq A\times B$.
    Then $\converse{R}\subseteq B\times A$.
\end{proposition}
\begin{proof}
    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}
    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}

\begin{proposition}\label{converse_subseteq_intro}
    Let $R$ be a relation.
    If $R\subseteq S$, then $\converse{R}\subseteq\converse{S}$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq,converse_relation,relation}.
\end{proof}

\begin{proposition}\label{converse_subseteq_elim}
    Let $R$ be a relation.
    If $\converse{R}\subseteq\converse{S}$, then $R\subseteq S$.
\end{proposition}
\begin{proof}
    Assume $\converse{R}\subseteq\converse{S}$.
    We have for all $x,y$ such that $x\mathrel{R}y$
        we have $x\mathrel{S}y$
        by \cref{subseteq,relation,converse_iff}.
    Follows by \cref{subseteq,relation}.
\end{proof}

\begin{proposition}\label{converse_subseteq_iff}
    Let $R$ be a relation.
    $\converse{R}\subseteq\converse{S}$ iff $R\subseteq S$.
\end{proposition}
\begin{proof}
    Follows by \cref{converse_subseteq_elim,converse_subseteq_intro}.
\end{proof}

\begin{proposition}\label{converse_union}
    $\converse{(R\union S)} = \converse{R}\union\converse{S}$.
\end{proposition}
\begin{proof}
    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}
    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}
    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}



\subsubsection{Domain of a relation}

\begin{definition}\label{dom}
    $\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$.
    Then $a\in\dom{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{dom_iff}.
\end{proof}

\begin{proposition}\label{dom_emptyset}
    $\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}

\begin{proposition}\label{dom_cons}
    $\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}

\begin{proposition}\label{dom_union}
    $\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}

\begin{proposition}\label{dom_inter}
    $\dom{(A\inter B)}\subseteq \dom{A}\inter\dom{B}$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq,inter,dom_iff}.
\end{proof}

\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}
%    Suppose $a\mathrel{R}b$.
%    Suppose $b\neq c$.
%    Then $\dom{\remove{(a,b)}{R}} = \dom{R}$.
%\end{proposition}

\subsubsection{Range of a relation}

\begin{definition}\label{ran}
    $\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$.
    Then $b\in\ran{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{ran_iff}.
\end{proof}

\begin{proposition}\label{ran_emptyset}
    $\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}

\begin{proposition}\label{ran_cons}
    $\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}

\begin{proposition}\label{ran_union}
    $\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}

\begin{proposition}\label{ran_inter}
    $\ran{(A\inter B)}\subseteq \ran{A}\inter\ran{B}$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq,inter,ran_iff}.
\end{proof}

\begin{proposition}\label{ran_setminus}
    $\ran{(A\setminus B)}\supseteq \ran{A}\setminus\ran{B}$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq,setminus,ran_iff}.
\end{proof}

\subsubsection{Domain and range of converse}

\begin{proposition}\label{dom_converse}
    $\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}

\begin{proposition}\label{ran_converse}
    $\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}


\subsubsection{Field of a relation}

% We ues fld for the label instead of field so that field stays available for the
% algebraic structure.
\begin{definition}\label{fld}
    $\fld{R} = \dom{R}\union\ran{R}$.
\end{definition}

\begin{proposition}\label{fld_iff}
    $c\in\fld{R}$ iff there exists $d$ such that $c\mathrel{R}d$ or $d\mathrel{R}c$.
\end{proposition}
\begin{proof}
    Follows by \cref{fld,dom_iff,ran_iff,union_iff}.
\end{proof}

\begin{proposition}\label{fld_intro_left}
    Suppose $(a,b)\in R$.
    Then $a\in\fld{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{fld,dom_iff,union_iff}.
\end{proof}

\begin{proposition}\label{fld_intro_right}
    Suppose $(a,b)\in R$.
    Then $b\in\fld{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{fld,ran_iff,union_iff}.
\end{proof}

\begin{proposition}\label{dom_subseteq_fld}
    Then $\dom{R}\subseteq\fld{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{fld,union_upper_left}.
\end{proof}

\begin{proposition}\label{ran_subseteq_fld}
    Then $\ran{R}\subseteq\fld{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{fld,union_upper_right}.
\end{proof}

\begin{proposition}\label{fld_times}
    $\fld{(A\times B)}\subseteq A\union B$.
\end{proposition}
\begin{proof}
    Follows by \cref{fld,dom_times,ran_times,union_subseteq_union}.
\end{proof}

\begin{proposition}\label{relation_elem_times_fld}
    Let $R$ be a relation.
    Suppose $w\in R$.
    Then $w\in\fld{R}\times\fld{R}$.
\end{proposition}
\begin{proof}
    Take $a,b$ such that $w = (a, b)$ by \cref{relation}.
    Then $a,b\in\fld{R}$ by \cref{fld_iff}.
    Thus $(a,b)\in\fld{R}\times\fld{R}$ by \cref{times_tuple_intro}.
\end{proof}

\begin{proposition}\label{relation_subseteq_times_fld}
    Let $R$ be a relation.
    Then $R\subseteq\fld{R}\times\fld{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{relation_elem_times_fld,subseteq}.
\end{proof}

\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}
    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}
    Follows by \cref{fld,dom_union,ran_union,union_comm,union_assoc}.
\end{proof}

\begin{proposition}\label{fld_inter}
    $\fld{(A\inter B)}\subseteq \fld{A}\inter\fld{B}$.
\end{proposition}
\begin{proof}
    % LATER this is surprisingly slow because the ATP can generate lots of nested intersection terms.
    Follows by \cref{subseteq,fld_iff,subseteq_inter_iff}.
\end{proof}

\begin{proposition}\label{fld_setminus}
    $\fld{(A\setminus B)}\supseteq \fld{A}\setminus\fld{B}$.
\end{proposition}
\begin{proof}
    Follows by \cref{setminus_subseteq,fld_iff,subseteq,setminus}.
\end{proof}

\begin{proposition}\label{fld_converse}
    $\fld{\converse{R}} = \fld{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{fld,dom_converse,ran_converse,union_comm}.
\end{proof}


\subsection{Image}

\begin{definition}\label{img}
    $\img{R}{A} = \{b\in\ran{R} \mid \exists a\in A. a\mathrel{R} b \}$.
\end{definition}

\begin{proposition}\label{img_elem_intro}
    Suppose $a\in A$ and $a\mathrel{R} b$.
    Then $b\in\img{R}{A}$.
\end{proposition}
\begin{proof}
    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$.
    Then $\img{R}{A}\subseteq \img{R}{B}$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq,img_iff}.
\end{proof}

\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}
    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}
    % Equality does not hold in general
    $\img{R}{A\inter B}\subseteq \img{R}{A}\inter\img{R}{B}$.
\end{proposition}
\begin{proof}
    Follows by \cref{img_iff,subseteq,inter}.
\end{proof}

\begin{proposition}\label{img_setminus}
    % Equality does not hold in general
    $\img{R}{A\setminus B}\supseteq \img{R}{A}\setminus\img{R}{B}$.
\end{proposition}
\begin{proof}
    Follows by \cref{img_iff,subseteq,setminus}.
\end{proof}

\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\}}$.
    Then $b\in\ran{R}$ and $(a,b)\in R$.
\end{proposition}
\begin{proof}
    Follows by \cref{img_iff,singleton_iff,img_subseteq_ran,elem_subseteq}.
\end{proof}

\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}

\subsection{Preimage}

\begin{definition}\label{preimg}
    $\preimg{R}{B} = \{a\in\dom{R} \mid \exists b\in B. a\mathrel{R} b \}$.
\end{definition}

\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}

\begin{proposition}\label{preimg_subseteq}
    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}

\begin{proposition}\label{preimg_inter}
    % 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}

\begin{definition}\label{upward_closure}
    $\upward{R}{a} = \{b\in\ran{R} \mid a\mathrel{R}b \}$.
\end{definition}

\begin{definition}\label{downward_closure}
    $\downward{R}{b} = \{a\in\dom{R} \mid a\mathrel{R}b \}$.
\end{definition}

\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}

Composition ignores the non-relational parts of sets.
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 = \{ 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}$ 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}
    Suppose $x\mathrel{(S\circ R)} z$.
    Then there exists $y$ such that $x\mathrel{R} y\mathrel{S} z$.
\end{proposition}
\begin{proof}
    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}
    Follows by \cref{relext,circ_is_relation,circ_iff}.
\end{proof}

\begin{proposition}\label{circ_converse_intro_tuple}
    Suppose $(a, c) \in\converse{R}\circ\converse{S}$.
    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$
        by \cref{circ_iff}.
    Now $c\mathrel{R}b\mathrel{S} a$ by \cref{converse_iff}.
    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}
    Suppose $(a,c)\in \converse{(S\circ R)}$.
    Then $(a, c) \in\converse{R}\circ\converse{S}$.
\end{proposition}
\begin{proof}
    $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}
    Follows by \cref{relext,converse_is_relation,circ_is_relation,circ_converse_intro_tuple,circ_converse_elim}.
\end{proof}

\subsection{Restriction}

\begin{definition}%
\label{restrl}
    $\restrl{R}{X} = \{ w\in R \mid \exists x, y. x\in X \land w = (x, y) \}$.
\end{definition}

\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}
    Suppose $x\in \dom{\restrl{R}{X}}$.
    Then $x\in \dom{R}, X$.
\end{proposition}
\begin{proof}
    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}%
\label{elem_dom_and_restr_implies_elem_of_restr}
    Suppose $x\in \dom{R}, X$.
    Then $x\in \dom{\restrl{R}{X}}$.
\end{proposition}
\begin{proof}
    Take $y$ such that $(x, y)\in R$ by \cref{dom_iff}.
    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}
    Suppose $R$ is a relation.
    $\restrl{R}{X} = R\inter (X\times \ran{R})$.
\end{proposition}
\begin{proof}
    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}.
    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}%
\label{dom_of_restrl_eq_inter}
    Suppose $R$ is a relation.
    $\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}

\begin{proposition}\label{restrl_restrl}
    Suppose $V\subseteq U$.
    Then $\restrl{\restrl{R}{U}}{V} = \restrl{R}{V}$.
\end{proposition}
\begin{proof}
    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 set extensionality.
\end{proof}

\begin{proposition}\label{restrl_by_dom}
    Let $R$ be a relation.
    Then $\restrl{R}{\dom{R}} = R$.
\end{proposition}
\begin{proof}
    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}$.
    Let $b\in\ran{\restrl{R}{X}}$.
    Then $b\in\img{R}{X}$.
\end{proposition}
\begin{proof}
    Follows by \cref{ran_iff,restrl_iff,img_iff}.
\end{proof}

\begin{proposition}\label{restrl_ran_intro}
    Suppose $X\subseteq\dom{R}$.
    Let $b\in\img{R}{X}$.
    Then $b\in\ran{\restrl{R}{X}}$.
\end{proposition}
\begin{proof}
    Follows by \cref{img,ran_intro,restrl_iff}.
\end{proof}

\begin{proposition}\label{restrl_ran}
    Suppose $X\subseteq\dom{R}$.
    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}

\begin{proposition}\label{restrl_img}
    Suppose $X\subseteq\dom{R}$.
    Then $\img{\restrl{R}{X}}{A} = \img{R}{X\inter A}$.
\end{proposition}
\begin{proof}
    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}.
    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}



\subsection{Set of relations}

% Also called "homogeneous relation" or "endorelation".
\begin{abbreviation}\label{binary_relation_on}
    $R$ is a binary relation on $X$ iff $R\subseteq X\times X$.
\end{abbreviation}

\begin{proposition}\label{relation_subseteq_intro_elem}
    Let $R$ be a relation.
    Suppose $\ran{R}\subseteq B$.
    Suppose $\dom{R}\subseteq A$.
    Suppose $w\in R$.
    Then $w\in A\times B$.
\end{proposition}
\begin{proof}
    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}
    Let $R$ be a relation.
    Suppose $\ran{R}\subseteq B$.
    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$.
    Suppose $a\in\dom{R}$.
    Then $a\in A$.
\end{proposition}
\begin{proof}
    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}
    Suppose $R\subseteq A\times B$.
    Then $\dom{R}\subseteq A$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq,relation_subseteq_implies_dom_subseteq_elem}.
\end{proof}

\begin{proposition}\label{relation_subseteq_implies_ran_subseteq_elem}
    Suppose $R\subseteq A\times B$.
    Suppose $b\in\ran{R}$.
    Then $b\in B$.
\end{proposition}
\begin{proof}
    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}
    Suppose $R\subseteq A\times B$.
    Then $\ran{R}\subseteq B$.
\end{proposition}
\begin{proof}
    Follows by \cref{subseteq,relation_subseteq_implies_ran_subseteq_elem}.
\end{proof}

\begin{definition}\label{rels}
    $\rels{A}{B} = \pow{A\times B}$.
\end{definition}

\begin{proposition}\label{rels_intro}
    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.
    Suppose $\dom{R}\subseteq A$.
    Suppose $\ran{R}\subseteq B$.
    Then $R\in\rels{A}{B}$.
\end{proposition}
\begin{proof}
    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}$.
    Then $\dom{R}\subseteq A$.
\end{proposition}
\begin{proof}
    Follows by \cref{rels_elim,relation_subseteq_implies_dom_subseteq}.
\end{proof}

\begin{proposition}\label{rels_ran_subseteq}
    Suppose $R\in\rels{A}{B}$.
    Then $\ran{R}\subseteq B$.
\end{proposition}
\begin{proof}
    Follows by \cref{rels_elim,relation_subseteq_implies_ran_subseteq}.
\end{proof}

\begin{proposition}\label{rels_is_relation}
    Let $R\in\rels{A}{B}$.
    Then $R$ is a relation.
\end{proposition}
\begin{proof}
    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}
    Let $R\in\rels{A}{B}$.
    Suppose $A\subseteq C$.
    Then $R\in\rels{C}{B}$.
\end{proposition}
\begin{proof}
    $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}
    Let $R\in\rels{A}{B}$.
    Suppose $B\subseteq D$.
    Then $R\in\rels{A}{D}$.
\end{proposition}
\begin{proof}
    $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}
    Let $R\in\rels{A}{B}$.
    Suppose $(a,b)\in R$.
    Then $(a,b)\in A\times B$.
\end{proposition}
\begin{proof}
    Follows by \cref{rels_elim,subseteq}.
\end{proof}

\begin{proposition}\label{rels_type_dom}
    Let $R\in\rels{A}{B}$.
    Suppose $(a,b)\in R$.
    Then $a\in A$.
\end{proposition}
\begin{proof}
    Follows by \cref{rels_type,times_tuple_elim}.
\end{proof}

\begin{proposition}\label{rels_type_ran}
    Let $R\in\rels{A}{B}$.
    Suppose $(a,b)\in R$.
    Then $b\in B$.
\end{proposition}
\begin{proof}
    Follows by \cref{rels_type,times_tuple_elim}.
\end{proof}

\begin{proposition}\label{rels_restrict_dom}
    Let $R\in\rels{A}{B}$.
    Then $R\in\rels{\dom{R}}{B}$.
\end{proposition}
\begin{proof}
    $R$ is a relation by \cref{rels_is_relation}.
    $\dom{R}\subseteq \dom{R}$ by \cref{subseteq_refl}.
    $\ran{R}\subseteq B$ by \cref{rels_ran_subseteq}.
    Follows by \cref{rels_intro_dom_and_ran}.
\end{proof}

\begin{proposition}\label{rels_restrict_ran}
    Let $R\in\rels{A}{B}$.
    Then $R\in\rels{A}{\ran{R}}$.
\end{proposition}
\begin{proof}
    $R$ is a relation by \cref{rels_is_relation}.
    $\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}

\subsection{Identity relation}

\begin{definition}\label{id}
    $\identity{A} = \{(a,a)\mid a\in A\}$.
\end{definition}

\begin{proposition}\label{id_iff}
    $a\mathrel{\identity{A}}b$ iff $a = b\in A$.
\end{proposition}
\begin{proof}
    Follows by \cref{id,pair_eq_iff}.
\end{proof}

\begin{proposition}\label{id_elem_intro}
    Suppose $a\in A$.
    Then $(a, a) \in\identity{A}$.
\end{proposition}
\begin{proof}
    Follows by \cref{id}.
\end{proof}

\begin{proposition}\label{id_elem_inspect}
    Suppose $w\in\identity{A}$.
    Then there exists $a\in A$ such that $w = (a, a)$.
\end{proposition}
\begin{proof}
    Follows by \cref{id}.
\end{proof}

\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}
    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}
    We have for all $a\in\ran{\identity{A}}$ we have $a\in A$
        by \cref{ran_iff,id_iff}.
    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}

\begin{definition}\label{memrel}
    $\memrel{A} = \{(a, b)\mid a\in A, b\in A \mid a\in b\}$.
\end{definition}

\begin{proposition}\label{memrel_elem_intro}
    Suppose $a, b\in A$.
    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}$.
    Then there exists $a, b\in A$ such that $w = (a, b)$ and $a\in b$.
\end{proposition}
\begin{proof}
    Follows by \cref{memrel}.
\end{proof}

\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}

\begin{definition}\label{subseteqrel}
    $\subseteqrel{A} = \{(a, b)\mid a\in A, b\in A \mid a\subseteq b\}$.
\end{definition}

\begin{proposition}\label{subseteqrel_is_relation}
    $\subseteqrel{A}$ is a relation.
\end{proposition}
\begin{proof}
    Follows by \cref{relation,subseteqrel}.
\end{proof}