\documentclass[../set-theory.tex]{subfiles}

\begin{document}
  \chapter{Zermelo's well-ordering theorem}\label{chapter:zermelo}

  \filename{set-theory/sections/05_well-ordering-theorem.ftl.tex}

  \begin{forthel}
    %[prove off][check off]

    [readtex \path{foundations/sections/13_equinumerosity.ftl.tex}]

    [readtex \path{set-theory/sections/04_recursion.ftl.tex}]

    %[prove on][check on]
  \end{forthel}


  \begin{forthel}
    \begin{theorem}[Zermelo]\printlabel{SET_THEORY_05_4227480655233024}
      Every set is equinumerous to some ordinal.
    \end{theorem}
    \begin{proof}
      Let $x$ be a set.

      [prover vampire]
      Every element of $(x \cup \set{x})^{< \infty}$ is a map. % Needed for ontological checking
      Define \[ G(F) =
        \begin{cases}
          \text{choose $u \in x \setminus \range(F)$ in $u$}
          & : x \setminus \range(F) \neq \emptyset
          \\
          x
          & : x \setminus \range(F) = \emptyset
        \end{cases} \]
      for $F \in (x \cup \set{x})^{< \infty}$.
      [prover eprover]

      Then $G$ is a map from $(x \cup \set{x})^{< \infty}$ to $x \cup \set{x}$.
      Indeed we can show that for any $F \in (x \cup \set{x})^{< \infty}$ we
      have $G(F) \in x \cup \set{x}$.
        Let $F \in (x \cup \set{x})^{< \infty}$.
        If $x \setminus \range(F) \neq \emptyset$ then
        $G(F) \in x \setminus \range(F)$.
        If $x \setminus \range(F) = \emptyset$ then $G(F) = x$.
        Hence $G(F) \in x \cup \set{x}$.
      End.
      Hence we can take a map $F$ from $\Ord$ to $x \cup \set{x}$ that is
      recursive regarding $G$.
      For any ordinal $\alpha$ we have $F \restriction \alpha \in
      (x \cup \set{x})^{< \infty}$.

      For any $\alpha \in \Ord$
      \[ x \setminus F[\alpha] \neq \emptyset \implies
      F(\alpha) \in x \setminus F[\alpha] \]
      and
      \[ x \setminus F[\alpha] = \emptyset \implies F(\alpha) = x. \]
      Proof.
        Let $\alpha \in \Ord$.
        We have $F[\alpha] = \{ F(\beta) \mid \beta \in \alpha \}$.
        Hence $F[\alpha] = \{ G(F \restriction \beta) \mid \beta \in \alpha \}$.
        We have $\range(F \restriction \alpha) =
        \{ F(\beta) \mid \beta \in \alpha \}$.
        Thus $\range(F \restriction \alpha) = F[\alpha]$.

        Case $x \setminus F[\alpha] \neq \emptyset$.
          Then $x \setminus \range(F \restriction \alpha) \neq \emptyset$.
          Hence $F(\alpha)
            = G(F \restriction \alpha)
            \in x \setminus \range(F \restriction \alpha)
            = x \setminus F[\alpha]$.
        End.

        Case $x \setminus F[\alpha] \neq \emptyset$.
          Then $x \setminus \range(F \restriction \alpha) = \emptyset$.
          Hence $F(\alpha)
            = G(F \restriction \alpha)
            = x$.
        End.
      Qed.

      (1) For any ordinals $\alpha, \beta$ such that $\alpha < \beta$ and
      $F(\beta) \neq x$ we have $F(\alpha), F(\beta) \in x$ and $F(\alpha) \neq
      F(\beta)$. \\
      Proof.
        Let $\alpha, \beta \in \Ord$.
        Assume $\alpha < \beta$ and $F(\beta) \neq x$.
        Then $x \setminus F[\beta] \neq \emptyset$.
        (a) Hence $F(\beta) \in x \setminus F[\beta]$.
        We have $F[\alpha] \subseteq F[\beta]$.
        Thus $x \setminus F[\alpha] \neq \emptyset$.
        (b) Therefore $F(\alpha) \in x \setminus F[\alpha]$.
        Consequently $F(\alpha), F(\beta) \in x$ (by a, b).
        We have $F(\alpha) \in F[\beta]$ and $F(\beta) \notin F[\beta]$.
        Thus $F(\alpha) \neq F(\beta)$.
      Qed.

      (2) There exists an ordinal $\alpha$ such that $F(\alpha) = x$. \\
      Proof.
        Assume the contrary.
        Then $F$ is a map from $\Ord$ to $x$.

        Let us show that $F$ is injective.
          Let $\alpha, \beta \in \Ord$.
          Assume $\alpha \neq \beta$.
          Then $\alpha < \beta$ or $\beta < \alpha$.
          Hence $F(\alpha) \neq F(\beta)$ (by 1).
          Indeed $F(\alpha), F(\beta) \neq x$.
        End.

        Thus $F$ is an injective map from some proper class to some set.
        Contradiction.
      Qed.

      Define $\Phi = \{ \alpha \in \Ord \mid F(\alpha) = x \}$.
      $\Phi$ is nonempty.
      Hence we can take a least element $\alpha$ of $\Phi$ regarding ${\in}$.
      Take $f = F \restriction \alpha$.
      Then $f$ is a map from $\alpha$ to $x$.
      Indeed for no $\beta \in \alpha$ we have $F(\beta) = x$.
      Indeed for all $\beta \in \alpha$ we have $(\beta, \alpha) \in {\in}$.

      (3) $f$ is surjective onto $x$. \\
      Proof.
        $x \setminus F[\alpha] = \emptyset$.
        Hence $\range(f)
          = f[\alpha]
          = F[\alpha]
          = x$.
      Qed.

      (4) $f$ is injective. \\
      Proof.
        Let $\beta, \gamma \in \alpha$.
        Assume $\beta \neq \gamma$.
        We have $f(\beta), f(\gamma) \neq x$.
        Hence $f(\beta) \neq f(\gamma)$ (by 1).
        Indeed $\beta < \gamma$ or $\gamma < \beta$.
      Qed.

      Therefore $f$ is a bijection between $\alpha$ and $x$.
      Consequently $x$ and $\alpha$ are equinumerous.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{SET_THEORY_05_689384265351168}
      For every set $x$ there exists a strong wellorder on $x$.
    \end{corollary}
    \begin{proof}
      Let $x$ be a set.
      Choose an ordinal $\alpha$ that is equinumerous to $x$.
      Take a bijection $f$ between $x$ and $\alpha$.
      Define $R = \{ (u,v) \mid u, v \in x$ and $f(u) < f(v) \}$.

      Let us show that $R$ is a strong wellorder on $x$.
        ${<}$ is a strong wellorder on $\alpha$.
        For all $u, v \in x$ we have $(u, v) \in R$ iff $f(u) < f(v)$.

        (1) $R$ is irreflexive on $x$.
        Indeed for all $u \in x$ we have $f(u) \nless f(u)$.

        (2) $R$ is transitive on $x$.
        Indeed for all $u, v, w \in x$ if $f(u) < f(v)$ and $f(v) < f(w)$ then
        $f(u) < f(w)$.

        (3) $R$ is connected on $x$. \\
        Proof.
          Let $u, v \in x$.
          Assume $u \neq v$.
          Then $f(u) \neq f(v)$.
          Hence $f(u) < f(v)$ or $f(v) < f(u)$ (by
          \cref{SET_THEORY_02_1718825707896832}).
          Indeed $f(u), f(v)$ are ordinals.
        Qed.

        Hence $R$ is a strict linear order on $x$.

        (4) $R$ is wellfounded on $x$. \\
        Proof.
          Let $A$ be a nonempty subclass of $x$.
          Then we can take a least element $\beta$ of $f[A]$ regarding
          ${<}$.
          Indeed $f[A]$ is a nonempty subclass of $\alpha$.
          Then $f^{-1}(\beta)$ is a least element of $A$ regarding $R$.
        Qed.

        We can show that for all $v \in x$ there exists a set $y$ such that
        $y = \{ u \in x \mid (u,v) \in R \}$.
          Let $v \in x$.
          Define $y = \{ u \in x \mid (u,v) \in R \}$.
          Then $y$ is a set such that $y = \{ u \in x \mid (u,v) \in R \}$.
        End.
        [prover vampire]
        Hence $R$ is strongly wellfounded on $x$ (by
        \cref{FOUNDATIONS_11_3262141912055808}).
        Indeed $R$ is a binary relation.
        Thus $R$ is a strong wellorder on $x$.
      End.
    \end{proof}
  \end{forthel}
\end{document}
