\documentclass[../arithmetic.tex]{subfiles}

\begin{document}
  \chapter{Cardinality}\label{chapter:cardinality}

  \filename{arithmetic/sections/11_cardinality.ftl.tex}

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

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

    [readtex \path{arithmetic/sections/04_ordering.ftl.tex}]

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


  \section{Subsections of the natural numbers}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_3625613501923328}
      Let $n, m$ be natural numbers.
      $\{ n, \dots, m \} = \{ k \in \Nat \mid n \leq k \leq m \}$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_145331933151232}
      Let $n, m$ be natural numbers.
      If $\{ 1, \dots, n \} = \{ 1, \dots, m \}$ then $n = m$.
    \end{proposition}
    \begin{proof}
      Assume $\{ 1, \dots, n \} = \{ 1, \dots, m \}$.

      Case $n = 0$.
        Then $\{ 1, \dots, n \} = \emptyset$.
        Thus $\{ 1, \dots, m \} = \emptyset$.
        Hence there exists no $k \in \Nat$ such that $1 \leq k \leq m$.
        Therefore $m = 0$.
        Consequently $n = m$.
      End.

      Case $m = 0$.
        Then $\{ 1, \dots, m \} = \emptyset$.
        Thus $\{ 1, \dots, n \} = \emptyset$.
        Hence there exists no $k \in \Nat$ such that $1 \leq k \leq n$.
        Therefore $n = 0$.
        Consequently $n = m$.
      End.

      Case $n, m \geq 1$.
        For all $k \in \Nat$ we have $1 \leq k \leq n$ iff $1 \leq k \leq m$.
        Hence for all $k \in \Nat$ we have $k \leq n$ iff $k \leq m$.

        Let us show by contradiction that $n = m$.
          Suppose $n \neq m$.
          Then $n > m$ or $m > n$.

          Case $n > m$.
            Take $k = m + 1$.
            Then $k \leq n$ and $k \nleq m$.
            Hence it is wrong that $k \leq n$ iff $k \leq m$.
            Contradiction.
          End.

          Case $m > n$.
            Take $k = n + 1$.
            Then $k \leq m$ and $k \nleq m$.
            Hence it is wrong that $k \leq n$ iff $k \leq m$.
            Contradiction.
          End.
        End.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_658708738605056}
      Let $n$ be a natural number.
      Then $\{ 1, \dots, n + 1 \} = \{ 1, \dots, n \} \cup \set{n + 1}$.
    \end{proposition}
    \begin{proof}
      We have
      $\{ 1, \dots, n + 1 \} \subseteq \{ 1, \dots, n \} \cup \set{n + 1}$ and
      $\{ 1, \dots, n \} \cup \set{n + 1} \subseteq \{ 1, \dots, n + 1 \}$.
    \end{proof}
  \end{forthel}


  \section{Finite and infinite sets}

  \paragraph{Finite sets}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_3694156977274880}
      Let $X$ be a set.
      $X$ is finite iff there exists a natural number $n$ such that $X$ is
      equinumerous to $\{ 1, \dots, n \}$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_3929085203972096}
      Let $X, Y$ be sets.
      If $X$ is finite and $Y$ is equinumerous to $X$ then $Y$ is finite.
    \end{proposition}
    \begin{proof}
      Assume that $X$ is finite and $Y$ is equinumerous to $X$.
      Take a natural number $n$ and a bijection $f$ between $\{ 1, \dots, n \}$
      and $X$ and a bijection $g$ between $X$ and $Y$.
      Then $g \circ f$ is a bijection between $\{ 1, \dots, n \}$ and $Y$
      (by \cref{FOUNDATIONS_08_6435206693126144}).
      Indeed $X, Y$ are classes.
      Hence $Y$ is finite.
    \end{proof}
  \end{forthel}


  \paragraph{Infinite sets}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_6612510618681344}
      Let $X$ be a set.
      $X$ is infinite iff $X$ is not finite.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_5814530911240192}
      Let $X, Y$ be sets.
      If $X$ is infinite and $Y$ is equinumerous to $X$ then $Y$ is infinite.
    \end{proposition}
    \begin{proof}
      Assume that $Y$ is equinumerous to $X$.
      If $Y$ is finite then $X$ is finite.
      Hence if $X$ is infinite then $Y$ is infinite.
    \end{proof}
  \end{forthel}


  \paragraph{The cardinality of a set}

  \begin{forthel}
    \begin{signature}\printlabel{ARITHMETIC_11_4604295827685376}
      $\infty$ is an object that is not a natural number.
    \end{signature}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_4220669648699392}
      Let $X$ be a set.
      The cardinality of $X$ is the object $\kappa$ such that

      (if $X$ is finite then $\kappa$ is the natural number $n$ such that $X$ is
      equinumerous to $\{ 1, \dots, n \}$) and

      if $X$ is infinite then $\kappa = \infty$.
    \end{definition}

    Let $|X|$ stand for the cardinality of $X$.

    Let $X$ has finitely many elements stand for $|X| \in \Nat$.
    Let $X$ has infinitely many elements stand for $|X| = \infty$.

    Let $X$ has exactly $n$ elements stand for $|X| = n$.
    Let $X$ has at most $n$ elements stand for $|X| \leq n$.
    Let $X$ has at least $n$ elements stand for $|X| \geq n$.
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_7260344969854976}
      Let $X$ be a set.
      $X$ is empty iff $|X| = 0$.
    \end{proposition}
    \begin{proof}
      Case $X$ is empty.
        Then $X = \emptyset = \{ 1, \dots, 0 \}$.
        Hence $X$ is equinumerous to $\{ 1, \dots, 0 \}$.
        Thus $|X| = 0$.
      End.

      Case $|X| = 0$.
        Then $X$ is equinumerous to $\{ 1, \dots, 0 \}$.
        $\{ 1, \dots, 0 \} = \emptyset$.
        Thus $X = \emptyset$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_963914846175232}
      Let $X$ be a set.
      $X$ is a singleton set iff $|X| = 1$.
    \end{proposition}
    \begin{proof}
      Case $X$ is a singleton set.
        Consider an object $a$ such that $X = \set{a}$.
        Define $f(x) = 1$ for $x \in X$.
        Then $f$ is a bijection between $X$ and $\set{1}$.
        We have $\set{1} = \{ 1, \dots, 1 \}$.
        Hence $|X| = 1$.
      End.

      Case $|X| = 1$.
        Take a bijection $f$ between $\{ 1, \dots, 1 \}$ and $X$.
        We have $\{ 1, \dots, 1 \} = \set{1}$.
        Hence $X = \set{f(1)}$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_3151583407767552}
      Let $X$ be a set.
      $X$ is an unordered pair iff $|X| = 2$.
    \end{proposition}
    \begin{proof}
      Case $X$ is an unordered pair.
        Consider distinct objects $a, b$ such that $X = \set{a, b}$.
        Define
        \[ f(x) =
          \begin{cases}
            1 & : x = a
            \\
            2 & : x = b
          \end{cases} \]
        for $x \in X$.
        Then $f$ is a bijection between $X$ and $\set{1, 2}$.
        We have $\{ 1, \dots, 2 \} = \set{1, 2}$.
        Hence $|X| = 2$.
      End.

      Case $|X| = 2$.
        Take a bijection $f$ between $\{ 1, \dots, 2 \}$ and $X$.
        We have $\{ 1, \dots, 2 \} = \set{1, 2}$.
        Hence $X = \set{f(1), f(2)}$.
      End.
    \end{proof}
  \end{forthel}


  \section{Countable and uncountable sets}

  \paragraph{Countably infinite sets}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_6249029537103872}
      Let $X$ be a set.
      $X$ is countably infinite iff $X$ is equinumerous to $\Nat$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_803449379749888}
      Let $X, Y$ be sets.
      If $X$ is countably infinite and $Y$ is equinumerous to $X$ then $Y$ is
      countably infinite.
    \end{proposition}
    \begin{proof}
      Assume that $X$ is countably infinite and $Y$ is equinumerous to $X$.
      Take a bijection $f$ between $\Nat$ and $X$ and a bijection $g$ between
      $X$ and $Y$.
      Then $g \circ f$ is a bijection between $\Nat$ and $Y$
      (by \cref{FOUNDATIONS_08_6435206693126144}).
      Indeed $X, Y$ are classes.
      Hence $Y$ is countably infinite.
    \end{proof}
  \end{forthel}


  \paragraph{Countable sets}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_5412969443753984}
      Let $X$ be a set.
      $X$ is countable iff $X$ is finite or $X$ is countably infinite.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_4182588499427328}
      Let $X, Y$ be sets.
      If $X$ is countable and $Y$ is equinumerous to $X$ then $Y$ is countable.
    \end{proposition}
    \begin{proof}
      Assume that $X$ is countable and $Y$ is equinumerous to $X$.
      If $X$ is finite then $Y$ is finite.
      If $X$ is countably infinite then $Y$ is countably infinite.
      Hence $Y$ is countable.
    \end{proof}
  \end{forthel}


  \paragraph{Uncountable sets}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_2411928395710464}
      Let $X$ be a set.
      $X$ is uncountable iff $X$ is not countable.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_1073385358491648}
      Let $X, Y$ be sets.
      If $X$ is uncountable and $Y$ is equinumerous to $X$ then $Y$ is
      uncountable.
    \end{proposition}
    \begin{proof}
      Assume that $Y$ is equinumerous to $X$.
      If $Y$ is countable then $X$ is countable.
      Hence if $X$ is uncountable then $Y$ is uncountable.
    \end{proof}
  \end{forthel}


  \section{Systems of sets}

  \paragraph{Definitions}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_1387314525765632}
      A system of finite sets is a system of sets $X$ such that every element of
      $X$ is finite.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_3786392159125504}
      A system of countably infinite sets is a system of sets $X$ such that
      every element of $X$ is countably infinite.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_7341152585908224}
      A system of countable sets is a system of sets $X$ such that every element
      of $X$ is countable.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_6106935677943808}
      A system of uncountable sets is a system of sets $X$ such that every
      element of $X$ is uncountable.
    \end{definition}
  \end{forthel}


  \paragraph{Closure under unions}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_3959378992431104}
      Let $X$ be a system of sets.
      $X$ is closed under arbitrary unions iff $\bigcup U \in X$ for every
      nonempty subset $U$ of $X$.
    \end{definition}

    Let $X$ is closed under unions stand for $X$ is closed under arbitrary
    unions.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_2377279311183872}
      Let $X$ be a system of sets.
      $X$ is closed under countable unions iff $\bigcup U \in X$ for every
      nonempty countable subset $U$ of $ X$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_7040118193913856}
      Let $X$ be a system of sets.
      $X$ is closed under finite unions iff $\bigcup U \in X$ for every nonempty
      finite subset $U$ of $X$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_4164024962908160}
      Let $X$ be a system of sets.
      $X$ is closed under finite unions iff $U \cup V \in X$ for every
      $U, V \in X$.
    \end{proposition}
    \begin{proof}
      Case $X$ is closed under finite unions.
        Let $U, V \in X$.
        Then $\set{U, V}$ is a nonempty finite subset of $X$.
        Hence $U \cup V = \bigcup \set{U, V} \in X$.
      End.

      Case $U \cup V \in X$ for every $U, V \in X$.
        Define $\Phi = \{ n \in \Nat \mid \bigcup U \in X$ for every nonempty
        subset $U$ of $X$ such that $|U| = n \}$.

        (1) $\Phi$ contains $0$.

        (2) For every $n \in \Phi$ we have $n + 1 \in \Phi$. \\
        Proof.
          Let $n \in \Phi$.
          Then $\bigcup U \in X$ for every nonempty subset $U$ of $X$ such that
          $|U| = n$.

          Let us show that $\bigcup U \in X$ for every nonempty subset $U$ of
          $X$ such that $|U| = n + 1$.

            Case $n = 0$. Obvious.

            Case $n \neq 0$.
              Let $U$ be a nonempty subset of $X$ such that $|U| = n + 1$.
              Take a bijection $f$ between $\{1, \dots, n + 1 \}$ and $U$.
              We have $\{ 1, \dots, n + 1 \} = \{ 1, \dots, n \} \cup \set{n + 1}$.
              Take $V = f[\{ 1, \dots, n \}]$.
              We have $\{ 1, \dots, n \} \subseteq \{ 1, \dots, n + 1 \}$.

              Let us show that $V \subseteq U$.
                Let $x \in V$.
                Take $k \in \{ 1, \dots, n \}$ such that $x = f(k)$.
                Hence $x \in U$.
              End.

              $V$ is a nonempty set.
              Hence $V$ is a nonempty subset of $X$.
              $U$ is a class and $f : \{ 1, \dots, n + 1 \} \into U$.
              [prover vampire]
              Hence $f \restriction \{ 1, \dots, n \}$ is a bijection between
              $\{ 1, \dots, n \}$ and $V$
              (by \cref{FOUNDATIONS_08_647446231252992}).
              [prover eprover]
              Thus $|V| = n$.
              Consequently $\bigcup V \in X$.
              We have $U = V \cup \set{f(n + 1)}$.
              Indeed $U = f[\{ 1, \dots, n + 1 \}]
                = f[\{ 1, \dots, n \} \cup \set{n + 1}]
                = f[\{ 1, \dots, n \}] \cup f[\set{n + 1}]
                = f[\{ 1, \dots, n \}] \cup \set{f(n + 1)}$.

              Let us show that $\bigcup (A \cup B) =
              (\bigcup A) \cup (\bigcup B)$ for any nonempty systems of sets
              $A, B$.
                Let $A, B$ be nonempty systems of sets.
                $\bigcup (A \cup B) \subseteq (\bigcup A) \cup (\bigcup B)$.
                $((\bigcup A) \cup (\bigcup B)) \subseteq \bigcup (A \cup B)$. %!
              End.

              Hence $\bigcup U
                = \bigcup (V \cup \set{f(n + 1)})
                = (\bigcup V) \cup (\bigcup \set{f(n + 1)})
                = (\bigcup V) \cup f(n + 1)
                \in X$.
              Indeed $V$ and $\set{f(n + 1)}$ are nonempty systems of sets.
            End.
          End.
        Qed.

        Therefore $\Phi$ contains every natural number.
        Thus $\bigcup U \in X$ for every nonempty finite subset $U$ of $X$.
        Consequently $X$ is closed under finite unions.
      End.
    \end{proof}
  \end{forthel}


  \paragraph{Closure under intersections}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_2369621166391296}
      Let $X$ be a system of sets.
      $X$ is closed under arbitrary intersections iff $\bigcap U \in X$ for
      every nonempty subset $U$ of $X$.
    \end{definition}

    Let $X$ is closed under intersections stand for $X$ is closed under
    arbitrary intersections.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_451771879129088}
      Let $X$ be a system of sets.
      $X$ is closed under countable intersections iff $\bigcap U \in X$ for
      every nonempty countable subset $U$ of $X$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_11_4297814324543488}
      Let $X$ be a system of sets.
      $X$ is closed under finite intersections iff $\bigcap U \in X$ for every
      nonempty finite subset $U$ of $X$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_11_1405012582334464}
      Let $X$ be a system of sets.
      $X$ is closed under finite intersections iff $U \cap V \in X$ for every
      $U, V \in X$.
    \end{proposition}
    \begin{proof}
      Case $X$ is closed under finite intersections.
        Let $U, V \in X$.
        Then $\set{U, V}$ is a nonempty finite subset of $X$.
        Hence $U \cap V = \bigcap \set{U, V} \in X$.
      End.

      Case $U \cap V \in X$ for every $U, V \in X$.
        Define $\Phi = \{ n \in \Nat \mid \bigcap U \in X$ for every nonempty
        subset $U$ of $X$ such that $|U| = n \}$.

        (1) $\Phi$ contains $0$.

        (2) For every $n \in \Phi$ we have $n + 1 \in \Phi$. \\
        Proof.
          Let $n \in \Phi$.
          Then $\bigcap U \in X$ for every nonempty subset $U$ of $X$ such that
          $|U| = n$.

          Let us show that $\bigcap U \in X$ for every nonempty subset $U$ of
          $X$ such that $|U| = n + 1$.

            Case $n = 0$. Obvious.

            Case $n \neq 0$.
              Let $U$ be a nonempty subset of $X$ such that $|U| = n + 1$.
              Take a bijection $f$ between $\{1, \dots, n + 1 \}$ and $U$.
              We have $\{ 1, \dots, n + 1 \} = \{ 1, \dots, n \} \cup \set{n + 1}$.
              Take $V = f[\{ 1, \dots, n \}]$.
              We have $\{ 1, \dots, n \} \subseteq \{ 1, \dots, n + 1 \}$.

              Let us show that $V \subseteq U$.
                Let $x \in V$.
                Take $k \in \{ 1, \dots, n \}$ such that $x = f(k)$.
                Hence $x \in U$.
              End.

              $V$ is a nonempty set.
              Hence $V$ is a nonempty subset of $X$.
              $U$ is a class and $f : \{ 1, \dots, n + 1 \} \into U$.
              [prover vampire]
              Hence $f \restriction \{ 1, \dots, n \}$ is a bijection between
              $\{ 1, \dots, n \}$ and $V$
              (by \cref{FOUNDATIONS_08_647446231252992}).
              [prover eprover]
              Thus $|V| = n$.
              Consequently $\bigcap V \in X$.
              We have $U = V \cup \set{f(n + 1)}$.
              Indeed $U = f[\{ 1, \dots, n + 1 \}]
                = f[\{ 1, \dots, n \} \cup \set{n + 1}]
                = f[\{ 1, \dots, n \}] \cup f[\set{n + 1}]
                = f[\{ 1, \dots, n \}] \cup \set{f(n + 1)}$.

              Let us show that $\bigcap (A \cup B) =
              (\bigcap A) \cap (\bigcap B)$ for any nonempty systems of sets
              $A, B$.
                Let $A, B$ be nonempty systems of sets.
                $\bigcap (A \cup B) \subseteq (\bigcap A) \cap (\bigcap B)$.
                $((\bigcap A) \cap (\bigcap B)) \subseteq \bigcap (A \cup B)$. %!
              End.

              Hence $\bigcap U
                = \bigcap (V \cup \set{f(n + 1)})
                = (\bigcap V) \cap (\bigcap \set{f(n + 1)})
                = (\bigcap V) \cap f(n + 1)
                \in X$.
              Indeed $V$ and $\set{f(n + 1)}$ are nonempty systems of sets.
            End.
          End.
        Qed.

        Therefore $\Phi$ contains every natural number.
        Thus $\bigcap U \in X$ for every nonempty finite subset $U$ of $X$.
        Consequently $X$ is closed under finite intersections.
      End.
    \end{proof}
  \end{forthel}
\end{document}
