\import{set.tex}

\section{Regularity}

\begin{abbreviation}\label{elemminimal}
    $a$ is an \in-minimal element of $A$ iff
    $a\in A$ and $a\notmeets A$.
\end{abbreviation}

% We need to first state regularity in this slightly weirder form,
% so that we can do \in-induction.
\begin{lemma}\label{regularity_aux}
    Suppose $a\in A$.
    Then there exists $b\in A$ such that
    $b\notmeets A$.
\end{lemma}
\begin{proof}[Proof by \in-induction on $a$]
    Follows by \cref{disjoint}.
\end{proof}

\begin{proposition}[Regularity]%
\label{regularity}
    Let $A$ be an inhabited set.
    Then there exists a \in-minimal element of $A$.
\end{proposition}
\begin{proof}
    Follows by \cref{regularity_aux}.
\end{proof}


% Foundation for case analysis
\begin{theorem}[Foundation]\label{foundation}
    Let $A$ be a set.
    Then $A = \emptyset$ or there exists $a\in A$
    such that for all $x\in a$ we have $x\notin A$.
\end{theorem}
\begin{proof}
    Follows by \cref{nonempty_inhabited,regularity,disjoint}.
\end{proof}.

\begin{proposition}\label{in_irrefl}
    For all sets $A$ we have $A\not\in A$.
\end{proposition}
\begin{proof}
    Follows by \cref{foundation,upair_iff}.
\end{proof}

\begin{proposition}\label{in_asymmetric}
    For all sets $a, b$ such that $a\in b$ we have $b\notin a$.
\end{proposition}
\begin{proof}
    Follows by \cref{foundation,upair_iff}.
\end{proof}