\section{Sets}

\begin{abbreviation}\label{ni}
    $A\ni a$ iff $a\in A$.
\end{abbreviation}

\subsection{Extensionality}

The axiom of set extensionality says that sets are determined by their \textit{extension},
that is, two sets are equal iff they have the same elements.
%
\begin{axiom}[Set extensionality]\label{setext}
    Suppose for all $a$ we have $a\in A$ iff $a\in B$.
    Then $A = B$.
\end{axiom}

This axiom is also available as the justification “{\ldots\ by set extensionality}”,
which applies it to goals of the form “$A = B$” and  “$A \neq B$”.

\begin{proposition}[Witness for disequality]%
\label{neq_witness}
    Suppose $A\neq B$.
    Then there exists $c$ such that
    either $c\in A$ and $c\not\in B$
    or $c\not\in A$ and $c\in B$.
\end{proposition}
\begin{proof}
    Suppose not. Then $A = B$ by set extensionality. Contradiction.
\end{proof}



\subsection{Subsets}

\begin{definition}\label{subseteq}
    $A\subseteq B$ iff
    for all $a\in A$ we have $a\in B$.
\end{definition}

\begin{abbreviation}\label{is_subset}
    $A$ is a subset of $B$ iff $A\subseteq B$.
\end{abbreviation}

\begin{abbreviation}\label{supseteq}
    $B\supseteq A$ iff $A\subseteq B$.
\end{abbreviation}

\begin{proposition}%
\label{subseteq_refl}
    $A\subseteq A$.
\end{proposition}

\begin{proposition}%
\label{subseteq_antisymmetric}
    Suppose $A\subseteq B\subseteq A$.
    Then $A = B$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{elem_subseteq}
    Suppose $a\in A\subseteq B$.
    Then $a\in B$.
\end{proposition}

\begin{proposition}%
\label{not_in_subseteq}
    Suppose $A\subseteq B$ and $c\notin B$.
    Then $c\notin A$.
\end{proposition}

\begin{proposition}%
\label{subseteq_transitive}
    Suppose $A\subseteq B\subseteq C$.
    Then $A\subseteq C$.
\end{proposition}

\begin{definition}\label{subset}
    $A\subset B$ iff
    $A\subseteq B$ and $A\neq B$.
\end{definition}

\begin{proposition}\label{subset_irrefl}
    $A\not\subset A$.
\end{proposition}

\begin{proposition}\label{subset_transitive}
    Suppose $A\subseteq B\subseteq C$.
    Then $A\subseteq C$.
\end{proposition}

\begin{proposition}\label{subset_witness}
    Suppose $A\subset B$.
    Then there exists $b\in B$ such that $b\notin A$.
\end{proposition}
\begin{proof}
    $A\subseteq B$ and $A\neq B$.
\end{proof}

\begin{abbreviation}\label{family_of_subsets}
    $F$ is a family of subsets of $X$ iff
    for all $A\in F$ we have $A\subseteq X$.
\end{abbreviation}


\subsection{The empty set}

\begin{axiom}%
\label{notin_emptyset}
    For all $a$ we have $a\notin\emptyset$.
\end{axiom}

\begin{definition}\label{inhabited}
    $A$ is inhabited iff
    there exists $a$ such that $a\in A$.
\end{definition}

\begin{abbreviation}\label{empty}
    $A$ is empty iff $A$ is not inhabited.
\end{abbreviation}

%\begin{proposition}%
%\label{inhabited_iff_nonempty}
%    $A$ is inhabited iff $A$ is not empty.
%\end{proposition}

\begin{proposition}%
\label{empty_eq}
    If $x$ and $y$ are empty, then $x = y$.
\end{proposition}

\begin{proposition}\label{emptyset_subseteq}
    For all $a$ we have $\emptyset \subseteq a$.
    % LATER $\emptyset$ is a subset of every set.
\end{proposition}

\begin{proposition}%
\label{subseteq_emptyset_iff}
    $A\subseteq \emptyset$ iff $A = \emptyset$.
\end{proposition}


\subsection{Disjointness of sets}

\begin{definition}\label{disjoint}
    $A$ is disjoint from $B$ iff there exists no $a$ such that $a\in A, B$.
\end{definition}

\begin{abbreviation}\label{notmeets}
    $A\notmeets B$ iff $A$ is disjoint from $B$.
\end{abbreviation}

\begin{abbreviation}\label{meets}
    $A\meets B$ iff $A$ is not disjoint from $B$.
\end{abbreviation}

\begin{proposition}%
\label{disjoint_symmetric}
    If $A$ is disjoint from $B$, then $B$ is disjoint from $A$.
\end{proposition}





\subsection{Unordered pairing and set adjunction}

Finite set expressions are desugared to
iterated application of $\operatorname{\textsf{cons}}$ to $\emptyset$.
Thus $\{x,y,z\}$ is an abbreviaton of
$\cons{x}{\cons{y}{\cons{z}{\emptyset}}}$.
The $\operatorname{\textsf{cons}}$ operation is determined by the following axiom:
%
\begin{axiom}\label{cons_iff}
    $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$.
\end{axiom}

\begin{proposition}\label{cons_left}
    $x\in \cons{x}{X}$.
\end{proposition}

\begin{proposition}\label{cons_right}
    If $y\in X$, then $y\in \cons{x}{X}$.
\end{proposition}


% Unordered pairs:

\begin{proposition}\label{upair_intro_left}
    $a\in\{a,b\}$.
\end{proposition}

\begin{proposition}\label{upair_intro_right}
    $b\in\{a,b\}$.
\end{proposition}

\begin{proposition}\label{upair_elim}
    Suppose $c\in\{a,b\}$. Then $a = c$ or $b = c$.
\end{proposition}

\begin{proposition}\label{upair_iff}
    $c\in\{a,b\}$ iff $a = c$ or $b = c$.
\end{proposition}


% Singletons:

\begin{proposition}\label{singleton_intro}
    $a\in\{a\}$.
\end{proposition}

\begin{proposition}\label{singleton_elim}
    If $a\in\{b\}$, then $a = b$.
\end{proposition}

\begin{proposition}\label{singleton_iff}
    $a\in\{b\}$ iff $a = b$.
\end{proposition}

\begin{abbreviation}\label{subsingleton}
    $A$ is a subsingleton iff for all $a, b\in A$ we have $a = b$.
\end{abbreviation}

\begin{proposition}\label{singleton_inhabited}
    $\{a\}$ is inhabited.
\end{proposition}

\begin{proposition}\label{singleton_iff_inhabited_subsingleton}
    Let $A$ be a subsingleton.
    Let $a\in A$.
    Then $A = \{a\}$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{singleton_subset_intro}
    Suppose $a\in C$.
    Then $\{a\}\subseteq C$.
\end{proposition}

\begin{proposition}\label{singleton_subset_elim}
    Suppose $\{a\}\subseteq C$.
    Then $a\in C$.
\end{proposition}


\subsection{Union and intersection}

\subsubsection{Union of a set}

\begin{axiom}\label{unions_iff}
    $z\in\unions{X}$ iff there exists $Y\in X$ such that $z\in Y$.
\end{axiom}


\begin{proposition}%
\label{unions_intro}
    Suppose $A\in B\in C$.
    Then $A\in\unions{C}$.
\end{proposition}
\begin{proof}
    There exists $B\in C$ such that $A\in B$.
\end{proof}

\begin{proposition}\label{unions_emptyset}
    $\unions{\emptyset} = \emptyset$.
\end{proposition}

\begin{proposition}\label{unions_family}
    Let $F$ be a family of subsets of $X$.
    Then $\unions{F}\subseteq X$.
\end{proposition}

\begin{abbreviation}\label{closedunderunions}
    $T$ is closed under arbitrary unions
    iff for every subset $M$ of $T$ we have $\unions{M}\in T$.
\end{abbreviation}

\subsubsection{Intersection of a set}

\begin{definition}\label{inters}
    $\inters{A} = \{ x\in\unions{A}\mid \text{for all $a\in A$ we have $x\in a$} \}$.
\end{definition}

\begin{proposition}\label{inters_iff_forall}
    $z\in\inters{X}$ iff $X$ is inhabited and for all $Y\in X$ we have $z\in Y$.
\end{proposition}

\begin{proposition}%
\label{inters_intro}
    Suppose $C$ is inhabited.
    Suppose for all $B\in C$ we have $A\in B$.
    Then $A\in\inters{C}$.
\end{proposition}

\begin{proposition}\label{inters_destr}
    Suppose $A\in\inters{C}$.
    Suppose $B\in C$.
    Then $A\in B$.
\end{proposition}

\begin{proposition}\label{inters_greatest}
    Suppose $A$ is inhabited.
    Suppose for all $a\in A$ we have $C\subseteq a$.
    Then $C\subseteq\inters{A}$.
\end{proposition}

\begin{proposition}\label{subseteq_inters_iff}
    Suppose $A$ is inhabited.
    Then $C\subseteq\inters{A}$ iff for all $a\in A$ we have $C\subseteq a$.
\end{proposition}

\begin{proposition}\label{inters_subseteq_elem}
    Let $B\in A$.
    Then $\inters{A}\subseteq B$.
\end{proposition}

\begin{proposition}\label{inters_singleton}
    $\inters{\{a\}} = a$.
\end{proposition}
\begin{proof}
    Every element of $a$ is an element of $\inters{\{a\}}$
        by \cref{inters_iff_forall,singleton_iff,singleton_inhabited}.
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{inters_emptyset}
    $\inters{\{\emptyset\}} = \emptyset$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\subsubsection{Binary union}

\begin{axiom}\label{union_iff}
    Let $A, B$ be sets.
    $a\in A\union B$ iff $a\in A$ or $a\in B$.
\end{axiom}

\begin{proposition}\label{union_intro_left}
    If $c\in A$, then $c\in A\union B$.
\end{proposition}

\begin{proposition}\label{union_intro_right}
    If $c\in B$, then $c\in A\union B$.
\end{proposition}

\begin{proposition}\label{union_as_unions}
    $\unions{\{x,y\}} = x\union y$.
\end{proposition}
\begin{proof}
    %For all z we have
    %\begin{align*}
    %    z\in \unions{\{x,y\}}
    %    &\iff \exists Z\in\{x,y\}. z\in Z
    %\end{align*}
    Follows by set extensionality.
\end{proof}

\begin{proposition}[Commutativity of union]%
\label{union_comm}
    $A\union B = B\union A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}[Associativity of union]%
\label{union_assoc}
    $(A\union B)\union C = A\union (B\union C)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}[Idempotence of union]%
\label{union_idempotent}
    $A\union A = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{union_subsets_is_subset}
    Suppose $A\subseteq C$ and $B\subseteq C$.
    Then $A\union B\subseteq C$.
\end{proposition}

\begin{proposition}\label{subseteq_union_iff}
    $A\union B\subseteq C$ iff $A\subseteq C$ and $B\subseteq C$.
\end{proposition}

\begin{proposition}\label{union_upper_left}
    $A\subseteq A\union B$.
\end{proposition}

\begin{proposition}\label{union_upper_right}
    $B\subseteq A\union B$.
\end{proposition}

\begin{proposition}\label{union_subseteq_union}
    Suppose $A\subseteq C$ and $B\subseteq D$.
    Then $A\union B\subseteq C\union D$.
\end{proposition}

\begin{proposition}%
\label{union_emptyset}
    $A\union\emptyset = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}


\begin{proposition}%
\label{union_emptyset_intro}
    Suppose $A = \emptyset$ and $B = \emptyset$. Then $A\union B = \emptyset$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{union_emptyset_elim_left}
    Suppose $A\union B = \emptyset$. Then $A = \emptyset$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{union_emptyset_elim_right}
    Suppose $A\union B = \emptyset$. Then $B = \emptyset$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{union_absorb_subseteq_left}
    Suppose $A\subseteq B$. Then $A\union B = B$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{union_absorb_subseteq_right}
    Suppose $A\subseteq B$. Then $B\union A = B$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{union_eq_self_implies_subseteq}
    If $A\union B = B$, then $A\subseteq B$.
\end{proposition}

\begin{proposition}\label{unions_cons}
    $\unions{\cons{b}{A}} = b\union\unions{A}$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{union_cons}
    $\cons{b}{A} \union C = \cons{b}{A\union C}$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{union_absorb_left}
    $A\union (A\union B) = A\union B$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{union_absorb_right}
    $(A\union B)\union B = A\union B$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{union_comm_left}
    $A\union (B\union C) = B\union (A\union C)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{abbreviation}\label{closedunderunion}
    $T$ is closed under binary unions
    iff for every $U,V\in T$ we have $U\union V\in T$.
\end{abbreviation}


\subsubsection{Binary intersection}

\begin{definition}\label{inter}
    $A\inter B = \{ a \in A \mid a\in B\}$.
\end{definition}

\begin{proposition}\label{inter_intro}
    If $c\in A, B$, then $c\in A\inter B$.
\end{proposition}

\begin{proposition}\label{inter_elim_left}
    If $c\in A\inter B$, then $c\in A$.
\end{proposition}

\begin{proposition}\label{inter_elim_right}
    If $c\in A\inter B$, then $c\in B$.
\end{proposition}

\begin{proposition}\label{inter_as_inters}
    $\inters{\{A,B\}} = A\inter B$.
\end{proposition}
\begin{proof}
    $\{A,B\}$ is inhabited.
    Thus for all $c$ we have $c\in\inters{\{A,B\}}$ iff $c\in A\inter B$
        by \cref{inters_iff_forall,inter,upair_iff}.
    %Thus $\inters{\{A,B\}} = A\inter B$ by \hyperref[setext]{extensionality}.
    Follows by \hyperref[setext]{extensionality}.
\end{proof}


\begin{proposition}[Commutativity of intersection]%
\label{inter_comm}
    $A\inter B = B\inter A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}[Associativity of intersection]%
\label{inter_assoc}
    $(A\inter B)\inter C = A\inter (B\inter C)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}[Idempotence of intersection]%
\label{inter_idempotent}
    $A\inter A = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{inter_emptyset}
    $A\inter\emptyset = \emptyset$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{inter_absorb_supseteq_right}
    Suppose $A\subseteq B$. Then $A\inter B = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{inter_absorb_supseteq_left}
    Suppose $A\subseteq B$. Then $B\inter A = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{inter_eq_left_implies_subseteq}
    Suppose $A\inter B = A$. Then $A\subseteq B$.
\end{proposition}

\begin{proposition}%
\label{subseteq_inter_iff}
    $C\subseteq A\inter B$ iff $C\subseteq A$ and $C\subseteq B$.
\end{proposition}

\begin{proposition}%
\label{inter_lower_left}
    $A\inter B \subseteq A$.
\end{proposition}

\begin{proposition}%
\label{inter_lower_right}
    $A\inter B \subseteq B$.
\end{proposition}

\begin{proposition}\label{inter_absorb_left}
    $A\inter (A\inter B) = A\inter B$.
\end{proposition}
\begin{proof} Follows by set extensionality. \end{proof}

\begin{proposition}%
\label{inter_absorb_right}
    $(A\inter B) \inter B = A\inter B$.
\end{proposition}
\begin{proof} Follows by set extensionality. \end{proof}

\begin{proposition}\label{inter_comm_left}
    $A\inter (B\inter C) = B\inter (A\inter C)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{inter_subseteq}
    Suppose $A,B\subseteq C$.
    Then $A\inter B\subseteq C$.
\end{proposition}

\begin{abbreviation}\label{closedunderinter}
    $T$ is closed under binary intersections
    iff for every $U,V\in T$ we have $U\inter V\in T$.
\end{abbreviation}

\subsubsection{Interaction of union and intersection}

\begin{proposition}[Binary intersection over binary union]%
\label{inter_distrib_union}
    $A\inter (B\union C) = (A\inter B)\union (A\inter C)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}[Binary union over binary intersection]%
\label{union_distrib_inter}
    $x\union (y\inter z) = (x\union y)\inter (x\union z)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

% Halmos, Naive Set Theory, page 16
\begin{proposition}\label{union_inter_assoc_intro}
    Suppose $C\subseteq A$.
    Then $A\inter (B\union C) = (A\inter B)\union C$.
\end{proposition}
\begin{proof}
    \begin{align*}
        A\inter (B\union C) &= (A\inter B)\union (A\inter C) \explanation{by \cref{inter_distrib_union}}\\
        &= (A\inter B)\union C \explanation{by \cref{inter_absorb_supseteq_left}}
    \end{align*}
\end{proof}

% Halmos, Naive Set Theory, page 16
\begin{proposition}\label{union_inter_assoc_elim}
    Suppose $(A\inter B)\union C = A\inter (B\union C)$.
    Then $C\subseteq A$.
\end{proposition}
\begin{proof}
    Follows by \cref{union_upper_right,union_upper_left,subseteq_union_iff,subseteq_antisymmetric,subseteq_inter_iff}.
\end{proof}

% From Isabelle/ZF equalities theory
\begin{proposition}\label{union_inter_crazy}
    $(A\inter B)\union (B\inter C)\union (C\inter A)
    =
    (A\union B)\inter (B\union C)\inter (C\union A)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}


\begin{proposition}[Intersection over binary union]\label{inters_distrib_union}
    Suppose $A$ and $B$ are inhabited.
    Then $\inters{A\union B} = (\inters{A})\inter\inters{B}$.
\end{proposition}
\begin{proof}
    $A\union B$ is inhabited.
    Thus for all $c$ we have $c\in\inters{A\union B}$ iff $c\in(\inters{A})\inter\inters{B}$
        by \cref{inter,union_iff,inters_iff_forall}.
    Follows by \hyperref[setext]{set extensionality}. % We only need the actual setext axiom here, not the tactic.
\end{proof}

\subsection{Set difference}

\begin{definition}\label{setminus}
    $A\setminus B = \{ a \in A \mid a\not\in B\}$.
\end{definition}

\begin{proposition}\label{setminus_intro}
    If $a\in A$ and $a\notin B$, then $a\in A\setminus B$.
\end{proposition}

\begin{proposition}\label{setminus_elim_left}
    If $a\in A\setminus B$, then $a\in A$.
\end{proposition}

\begin{proposition}\label{setminus_elim_right}
    If $a\in A\setminus B$, then $a\notin B$.
\end{proposition}

\begin{proposition}\label{setminus_emptyset}
    $x\setminus \emptyset = x$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{emptyset_setminus}
    $\emptyset\setminus x = \emptyset$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{setminus_self}
    $x\setminus x = \emptyset$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

% NOTE: This theorem tends to show up spuriously in ATP proofs!
% Getting rid of it via explicit \cref{..} can save time.
\begin{proposition}\label{setminus_setminus}
    $x\setminus (x\setminus y) = x\inter y$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{double_relative_complement}
    Suppose $y\subseteq x$.
    $x\setminus (x\setminus y) = y$.
\end{proposition}
\begin{proof}
    Follows by \cref{setminus_setminus,inter_absorb_supseteq_left}.
\end{proof}

\begin{proposition}\label{setminus_inter}
    $x\setminus (y\inter z) = (x\setminus y)\union (x\setminus z)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{setminus_union}
    $x\setminus (y\union z) = (x\setminus y)\inter (x\setminus z)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{inter_setminus}
    $x\inter (y\setminus z) = (x\inter y)\setminus (x\inter z)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}%
\label{difference_with_proper_subset_is_inhabited}
    Let $A, B$ be sets.
    Suppose $A\subset B$.
    Then $B\setminus A$ is inhabited.
\end{proposition}
\begin{proof}
    Take $b$ such that $b\in B$ and $b\notin A$.
    Then $b\in B\setminus A$.
\end{proof}

\begin{proposition}\label{setminus_subseteq}
    $B\setminus A\subseteq B$.
\end{proposition}

\begin{proposition}\label{subseteq_setminus}
    Suppose $C\subseteq A$.
    Suppose $C\inter B = \emptyset$.
    Then $C\subseteq A\setminus B$.
\end{proposition}


\begin{proposition}\label{subseteq_implies_setminus_supseteq}
    Suppose $A\subseteq B$.
    Then $C\setminus A\supseteq C\setminus B$.
\end{proposition}

\begin{proposition}\label{setminus_absorb_right}
    Suppose $A\inter B = \emptyset$.
    Then $A\setminus B = A$.
\end{proposition}

\begin{proposition}\label{setminus_eq_emptyset_iff_subseteq}
    $A\setminus B = \emptyset$ iff $A\subseteq B$.
\end{proposition}

\begin{proposition}\label{subseteq_setminus_cons_intro}
    Suppose $B\subseteq A\setminus C$ and $c\notin B$. Then $B\subseteq A\setminus\cons{c}{C}$.
\end{proposition}

\begin{proposition}\label{subseteq_setminus_cons_elim}
    Suppose $B\subseteq A\setminus\cons{c}{C}$. Then $B\subseteq A\setminus C$ and $c\notin B$.
\end{proposition}

\begin{proposition}\label{setminus_cons}
    $A\setminus \cons{a}{B} = (A\setminus \{a\})\setminus B$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}
\begin{proposition}\label{setminus_cons_flip}
    $A\setminus \cons{a}{B} = (A\setminus B)\setminus \{a\}$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{setminus_disjoint}
    $A\inter (B\setminus A) = \emptyset$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{setminus_partition}
    Suppose $A\subseteq B$.
    $A\union (B\setminus A) = B$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{subseteq_union_setminus}
    $A\subseteq B\union (A\setminus B)$.
\end{proposition}

\begin{proposition}\label{double_complement}
    Suppose $A\subseteq B\subseteq C$.
    Then $B\setminus (C\setminus A) = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{double_complement_union}
    Then $(A\union B)\setminus (B\setminus A) = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{setminus_eq_inter_complement}
    Suppose $A, B\subseteq C$.
    Then $A\setminus B = A\inter (C\setminus B)$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\subsection{Tuples}

As with unordered pairs,
orderd pairs are a primitive construct and
$n$-tuples desugar to iterated applications of the
primitive operator $({-},{-})$.
For example $(a, b, c, d)$ equals $(a, (b, (c, d)))$ by definition.
While ordered pairs could be encoded set-theoretically, %(choosing Kuratowski's, Hausdorff's, or Wiener's encoding),
we simply postulate the defining property to prevent misguiding
proof automation.

\begin{axiom}\label{pair_eq_iff}
    $(a, b) = (a', b')$ iff $a = a'\land b = b'$.
\end{axiom}

\begin{axiom}\label{pair_neq_emptyset}
    $(a, b) \neq \emptyset$.
\end{axiom}

\begin{axiom}\label{pair_neq_fst}
    $(a, b) \neq a$.
\end{axiom}

\begin{axiom}\label{pair_neq_snd}
    $(a, b) \neq b$.
\end{axiom}

Repeated application of the defining property of pairs yields the defining property of
all tuples.

\begin{proposition}\label{triple_eq_iff}
    $(a, b, c) = (a', b', c')$ iff $a = a' \land b = b'\land c = c'$.
\end{proposition}

There are primitive projections $\fst{}$ and $\snd{}$ that satisfy the following axioms.

\begin{axiom}\label{fst_eq}
    $\fst{(a, b)} = a$.
\end{axiom}

\begin{axiom}\label{snd_eq}
    $\snd{(a, b)} = b$.
\end{axiom}

\begin{proposition}\label{pair_eq_pair_of_proj}
    $(a, b) = (\fst{(a,b)},\snd{(a,b)})$.
\end{proposition}


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

\begin{proposition}\label{times_tuple_elim}
    Suppose $(x, y)\in X\times Y$. Then $x\in X$ and $y\in Y$.
\end{proposition}
\begin{proof}
    Take $x', y'$ such that $x'\in X\land y'\in Y \land (x, y) = (x', y')$
        by \cref{times}.
    Then $x = x'$ and $y = y'$ by \cref{pair_eq_iff}.
\end{proof}

\begin{proposition}\label{times_tuple_intro}
    Suppose $x\in X$ and $y\in Y$. Then $(x, y)\in X\times Y$.
\end{proposition}

\begin{proposition}\label{times_empty_left}
    $\emptyset\times Y = \emptyset$.
\end{proposition}

\begin{proposition}\label{times_empty_right}
    $X\times \emptyset = \emptyset$.
\end{proposition}

\begin{proposition}\label{times_empty_iff}
    $X\times Y$ is empty iff $X$ is empty or $Y$ is empty.
\end{proposition}
\begin{proof}
    Follows by \cref{inhabited,times}.
\end{proof}

\begin{proposition}\label{fst_type}
    Suppose $c\in A\times B$. Then $\fst{c}\in A$.
\end{proposition}
\begin{proof}
    Take $a, b$ such that $c = (a, b)$ and $a\in A$
        by \cref{times}.
    $a = \fst{c}$
        by \cref{fst_eq}.
\end{proof}

\begin{proposition}\label{snd_type}
    Suppose $c\in A\times B$. Then $\snd{c}\in B$.
\end{proposition}
\begin{proof}
    Take $a, b$ such that $c = (a, b)$ and $b\in B$
        by \cref{times}.
    $b = \snd{c}$
        by \cref{snd_eq}.
\end{proof}

\begin{proposition}\label{times_elem_is_tuple}
    Suppose $p\in X\times Y$. Then there exist $x, y$
    such that $x\in X$ and $y\in Y$ and $p = (x, y)$.
\end{proposition}


\begin{proposition}\label{times_proj_elim}
    Suppose $p\in X\times Y$. Then $\fst{p}\in X$ and $\snd{p}\in Y$.
\end{proposition}