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

\begin{document}
  \chapter{Finite ordinals}\label{chapter:finite-ordinals}

  \filename{set-theory/sections/03_finite-ordinals.ftl.tex}

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

    [readtex \path{set-theory/sections/02_ordinals.ftl.tex}]

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


  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_03_4310076227584000}
      \[ \omega = \class{n \in \Ord | \classtext{$n \in X$ for every
      $X \subseteq \Ord$ such that $0 \in X$ and for all $x \in X$ we have
      $\succ(x) \in X$}}. \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_3576717620805632}
      $0 \in \omega$.
    \end{proposition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_8807317141192704}
      Let $n \in \omega$.
      Then $\succ(n) \in \omega$.
    \end{proposition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_344585425387520}
      Let $\Phi \subseteq \omega$.
      Assume that $0 \in \Phi$ and for every $x \in \Phi$ we have
      $\succ(x) \in \Phi$.
      Then $\Phi = \omega$.
    \end{proposition}
    \begin{proof}
      Suppose $\Phi \neq \omega$.
      Consider an element $n$ of $\omega$ that is not contained in $\Phi$.
      Take $\Phi' = \Phi \setminus \set{n}$.

      (1) $0 \in \Phi'$.
      Indeed $0 \in \Phi$ and $0 \neq n$.

      (2) For each $x \in \Phi'$ we have $\succ(x) \in \Phi'$. \\
      Proof.
        Let $x \in \Phi'$.
        Then $\succ(x) \in \Phi$.

        Let us show that $\succ(x) \neq n$.
          Assume $\succ(x) = n$.
          Then $x \notin \Phi$.
          Indeed $n \notin \Phi$ and if $x \in \Phi$ then
          $n = \succ(x) \in \Phi$.
          Contradiction.
        End.

        Thus $\succ(x) \in \Phi'$.
      Qed.

      Therefore every element of $\omega$ lies in $\Phi'$.
      Indeed $\Phi' \subseteq \Ord$.
      Consequently $n \in \Phi'$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{SET_THEORY_03_4847727433220096}
      $\omega$ is a set.
    \end{corollary}
    \begin{proof}
      Define $f(n) = \succ(n)$ for $n \in \omega$.
      Take a subset $X$ of $\omega$ that is inductive regarding $0$ and $f$.
      Indeed $f$ is a map from $\omega$ to $\omega$.
      Then we have $0 \in X$ and for each $n \in X$ we have $\succ(n) \in X$.
      Thus $X = \omega$.
      Therefore $\omega$ is a set.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_5885789275684864}
      Let $n \in \omega$.
      Then $n = 0$ or $n = \succ(m)$ for some $m \in \omega$.
    \end{proposition}
    \begin{proof}
      Assume the contrary.
      Consider a $k \in \omega$ such that neither $k = 0$ nor $k = \succ(m)$ for
      some $m \in \omega$.
      Take a class $\omega'$ such that $\omega' = \omega \setminus \set{k}$. %!
      Then $\omega'$ is a set.

      (1) $0 \in \omega'$.
      Indeed $k \neq 0$.

      (2) For all $m \in \omega'$ we have $\succ(m) \in \omega'$. \\
      Proof.
        Let $m \in \omega'$.
        Then $\succ(m) \neq k$.
        Hence $\succ(m) \in \omega'$.
      Qed.

      Thus every element of $\omega$ is contained in $\omega'$.
      Therefore $k \in \omega'$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_5057540872208384}
      Every element of $\omega$ is an ordinal.
    \end{proposition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_764451995254784}
      $\omega$ is a limit ordinal.
    \end{proposition}
    \begin{proof}
      $\omega$ is transitive. \\
      Proof.
        Define $\Phi = \{ n \in \omega \mid$ for all $m \in n$ we have
        $m \in \omega \}$.

        (1) $0 \in \Phi$.

        (2) For all $n \in \Phi$ we have $\succ(n) \in \Phi$. \\
        Proof.
          Let $n \in \Phi$.
          Then every element of $n$ is contained in $\omega$.
          Hence every element of $\succ(n)$ is contained in $\omega$.
          Thus $\succ(n) \in \Phi$.
        Qed.

        Therefore $\omega \subseteq \Phi$.
        Consequently $\omega$ is transitive.
      Qed.

      Every element of $\omega$ is an ordinal.
      Hence every element of $\omega$ is transitive.
      Thus $\omega$ is an ordinal.

      $\omega$ is a limit ordinal. \\
      Proof.
        Assume the contrary.
        We have $\omega \neq 0$.
        Hence $\omega$ is a successor ordinal.
        Take an ordinal $\alpha$ such that $\succ(\alpha) = \omega$.
        Then $\alpha \in \omega$.
        Thus $\omega = \succ(\alpha) \in \omega$.
        Contradiction.
      Qed.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_5517271459954688}
      Let $\lambda$ be a limit ordinal.
      Then \[ \omega \leq \lambda. \]
    \end{proposition}
    \begin{proof}
      Assume the contrary.
      Then $\lambda < \omega$.
      Consequently $\lambda \in \omega$.
      Hence $\lambda = 0$ or $\lambda = \succ(n)$ for some $n \in \omega$.
      Thus $\lambda$ is not a limit ordinal.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_03_1991057988386816}
      $1 = \succ(0)$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_03_5809204518453248}
      $2 = \succ(1)$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_4388003120152576}
      $1 = \set{0}$.
    \end{proposition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_930896899211264}
      $2 = \set{0,1}$.
    \end{proposition}
  \end{forthel}
\end{document}
