\begin{proposition}\label{prelude_universe_contains}
    For all $n$ we have $n \in \cumul{n}$.
\end{proposition}

\begin{proposition}\label{prelude_universe_transitive}
    For all $n, a$ we have if $a \in \cumul{n}$, then for all $x$ if $x \in a$, then $x \in \cumul{n}$.
\end{proposition}

\begin{proposition}\label{prelude_universe_union_closed}
    For all $n, a$ we have if $a \in \cumul{n}$, then $\unions{a} \in \cumul{n}$.
\end{proposition}

\begin{proposition}\label{prelude_universe_power_closed}
    For all $n, a$ we have if $a \in \cumul{n}$, then $\pow{a} \in \cumul{n}$.
\end{proposition}

\begin{proposition}\label{setext}
    For all $A,B$ we have if for all $x$ if $x \in A$, then $x \in B$, then if for all $x$ if $x \in B$, then $x \in A$, then $A = B$.
\end{proposition}

\begin{proposition}\label{emptyset}
    For all $x$ we have $x \in \emptyset$ iff $\bot$.
\end{proposition}

\begin{proposition}\label{pairset_iff}
    For all $a,b,x$ we have $x \in \upair{a}{b}$ iff $x = a$ or $x = b$.
\end{proposition}

\begin{proposition}\label{pow_iff}
    For all $A,B$ we have $B \in \pow{A}$ iff for all $x$ if $x \in B$, then $x \in A$.
\end{proposition}

\begin{proposition}\label{unions_iff}
    For all $A,x$ we have $x \in \unions{A}$ iff there exists $B \in A$ such that $x \in B$.
\end{proposition}

\begin{definition}\label{prelude_successor}
    $\preludeSuccessor{x} = \unions{\upair{\upair{x}{x}}{x}}$.
\end{definition}

\begin{definition}\label{prelude_transitive}
    $\preludeTransitive{A}$ iff for all $x$ we have if $x \in A$, then for all $y$ if $y \in x$, then $y \in A$.
\end{definition}

\begin{definition}\label{prelude_inductive}
    $\preludeInductive{A}$ iff it is not the case that if $\emptyset \in A$, then it is not the case that for all $x$ we have if $x \in A$, then $\preludeSuccessor{x} \in A$.
\end{definition}

\begin{definition}\label{prelude_u0}
    $\preludeU = \cumul{\emptyset}$.
\end{definition}

\begin{proposition}\label{prelude_u0_empty}
    $\emptyset \in \preludeU$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_universe_contains,prelude_u0}.
\end{proof}

\begin{proposition}\label{prelude_empty_transitive}
    $\preludeTransitive{\emptyset}$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_transitive}.
\end{proof}

\begin{proposition}\label{prelude_successor_transitive}
    For all $x$ we have if $\preludeTransitive{x}$, then $\preludeTransitive{\preludeSuccessor{x}}$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_transitive,prelude_successor}.
\end{proof}

\begin{proposition}\label{prelude_successor_power_bound}
    For all $x$ we have if $\preludeTransitive{x}$, then $\preludeSuccessor{x} \in \pow{\pow{x}}$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_transitive,prelude_successor}.
\end{proof}

\begin{proposition}\label{prelude_u0_transitive_successor}
    For all $x$ we have if $x \in \preludeU$, then if $\preludeTransitive{x}$, then $\preludeSuccessor{x} \in \preludeU$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_universe_transitive,prelude_universe_power_closed,prelude_successor_power_bound,prelude_u0}.
\end{proof}

\begin{definition}\label{prelude_transitive_part}
    $\preludeTransitivePart = \{ x \in \preludeU \mid \preludeTransitive{x} \}$.
\end{definition}

\begin{proposition}\label{prelude_transitive_part_empty}
    $\emptyset \in \preludeTransitivePart$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_transitive_part,prelude_u0_empty,prelude_empty_transitive}.
\end{proof}

\begin{proposition}\label{prelude_transitive_part_successor}
    For all $x$ we have if $x \in \preludeTransitivePart$, then $\preludeSuccessor{x} \in \preludeTransitivePart$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_transitive_part,prelude_u0_transitive_successor,prelude_successor_transitive}.
\end{proof}

\begin{proposition}\label{prelude_infinity}
    $\preludeInductive{\preludeTransitivePart}$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_inductive,prelude_transitive_part_empty,prelude_transitive_part_successor}.
\end{proof}

\begin{definition}\label{prelude_omega}
    $\preludeOmega = \{ x \in \preludeU \mid \text{for all $A$ if $\preludeInductive{A}$, then $x \in A$} \}$.
\end{definition}

\begin{proposition}\label{prelude_omega_empty}
    $\emptyset \in \preludeOmega$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_omega,prelude_u0_empty,prelude_inductive}.
\end{proof}

\begin{proposition}\label{prelude_omega_successor}
    For all $x$ we have if $x \in \preludeOmega$, then $\preludeSuccessor{x} \in \preludeOmega$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_omega,prelude_infinity,prelude_transitive_part,prelude_u0_transitive_successor,prelude_inductive}.
\end{proof}

\begin{proposition}\label{prelude_omega_inductive}
    $\preludeInductive{\preludeOmega}$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_inductive,prelude_omega_empty,prelude_omega_successor}.
\end{proof}

\begin{proposition}\label{prelude_omega_minimal}
    For all $A$ we have if $\preludeInductive{A}$, then for all $x$ if $x \in \preludeOmega$, then $x \in A$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_omega}.
\end{proof}

\begin{abbreviation}\label{prelude_naturals}
    $\naturals = \preludeOmega$.
\end{abbreviation}

\begin{proposition}\label{prelude_naturals_inductive}
    $\preludeInductive{\naturals}$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_omega_inductive}.
\end{proof}

\begin{proposition}\label{prelude_naturals_minimal}
    For all $A$ we have if $\preludeInductive{A}$, then for all $x$ if $x \in \naturals$, then $x \in A$.
\end{proposition}
\begin{proof}
    Follows by \cref{prelude_omega_minimal}.
\end{proof}