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

\begin{document}
  \chapter{Equinumerosity}\label{chapter:equinumerosity}

  \filename{foundations/sections/13_equinumerosity.ftl.tex}

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

    [readtex \path{foundations/sections/12_fixed-points.ftl.tex}]

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


  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_13_4578620297183232}
      Let $A, B$ be classes.
      $A$ is equinumerous to $B$ iff there exists a bijection between $A$ and
      $B$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_13_3703161885818880}
      Let $A$ be a class.
      Then $A$ is equinumerous to $A$.
    \end{proposition}
    \begin{proof}
      $\id_{A}$ is a bijection between $A$ and $A$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_13_8050301789536256}
      Let $A, B$ be classes.
      If $A$ and $B$ are equinumerous then $B$ and $A$ are equinumerous.
    \end{proposition}
    \begin{proof}
      Assume that $A$ and $B$ are equinumerous.
      Take a bijection $f$ between $A$ and $B$.
      Then $f^{-1}$ is a bijection between $B$ and $A$.
      Hence $B$ and $A$ are equinumerous.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_13_3609912414306304}
      Let $A, B, C$ be classes.
      If $A$ and $B$ are equinumerous and $B$ and $C$ are equinumerous then
      $A$ and $C$ are equinumerous.
    \end{proposition}
    \begin{proof}
      Assume that $A$ and $B$ are equinumerous and $B$ and $C$ are
      equinumerous.
      Take a bijection $f$ between $A$ and $B$ and a bijection $g$ between
      $B$ and $C$.
      Then $g \circ f$ is a bijection between $A$ and $C$.
      Hence $A$ and $C$ are equinumerous.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}[Cantor-Schröder-Bernstein]\printlabel{FOUNDATIONS_13_1913663275401216}
      Let $x, y$ be sets.
      Then $x$ and $y$ are equinumerous iff there exists an injective map from
      $x$ to $y$ and there exists an injective map from $y$ to $x$.
    \end{theorem}
    \begin{proof}
      Case $x$ and $y$ are equinumerous.
        Take a bijection $f$ between $x$ and $y$.
        Then $f^{-1}$ is a bijection between $y$ and $x$.
        Hence $f$ is an injective map from $x$ to $y$ and $f^{-1}$ is an
        injective map from $y$ to $x$.
      End.

      Case there exists an injective map from $x$ to $y$ and there exists an
      injective map from $y$ to $x$.
        Take an injective map $f$ from $x$ to $y$.
        Take an injective map $g$ from $y$ to $x$.
        We have $y \setminus f[a] \subseteq y$ for any $a \in \pow(x)$.

        (1) Define $h(a) = x \setminus g[y \setminus f[a]]$ for $a \in \pow(x)$.

        $h$ is a map from $\pow(x)$ to $\pow(x)$.
        Indeed $h(a)$ is a subset of $x$ for each subset $a$ of $x$.

        Let us show that $h$ is subset preserving.
          Let $u, v$ be subsets of $x$.
          Assume $u \subseteq v$.
          Then $f[u] \subseteq f[v]$.
          Hence $y \setminus f[v] \subseteq y \setminus f[u]$.
          Thus $g[y \setminus f[v]] \subseteq g[y \setminus f[u]]$.
          Indeed $y \setminus f[v]$ and $y \setminus f[u]$ are subsets of $y$.
          Therefore $x \setminus g[y \setminus f[u]] \subseteq
          x \setminus g[y \setminus f[v]]$.
          Consequently $h[u] \subseteq h[v]$.
        End.

        Hence we can take a fixed point $c$ of $h$ (by
        \cref{FOUNDATIONS_12_8420450166112256}).

        (2) Define $F(u) = f(u)$ for $u \in c$.

        We have $c = h(c)$ iff $x \setminus c = g[y \setminus f[c]]$.
        $g^{-1}$ is a bijection between $\range(g)$ and $y$.
        Thus $x \setminus c = g[y \setminus f[c]] \subseteq \range(g)$.
        Therefore $x \setminus c$ is a subset of $\dom(g^{-1})$.

        (3) Define $G(u) = g^{-1}(u)$ for $u \in x \setminus c$.

        $F$ is a bijection between $c$ and $\range(F)$.
        $G$ is a bijection between $x \setminus c$ and $\range(G)$.

        Define \[ H(u) =
          \begin{cases}
            F(u) & : u \in c \\
            G(u) & : u \notin c
          \end{cases} \]
        for $u \in x$.

        Let us show that $H$ is a map to $y$.
          $\dom(H)$ is a set and every value of $H$ is an object.
          Hence $H$ is a map.

          Let us show that every value of $H$ lies in $y$.
            Let $v$ be a value of $H$.
            Take $u \in x$ such that $H(u) = v$.
            If $u \in c$ then $v = H(u) = F(u) = f(u) \in y$.
            If $u \notin c$ then $v = H(u) = G(u) = g^{-1}(u) \in y$.
          End.
        End.

        (4) $H$ is surjective onto $y$.
        Indeed we can show that every element of $y$ is a value of $H$.
          Let $v \in y$.

          Case $v \in f[c]$.
            Take $u \in c$ such that $f(u) = v$.
            Then $F(u) = v$.
          End.

          Case $v \notin f[c]$.
            Then $v \in y \setminus f[c]$.
            Hence $g(v) \in g[y \setminus f[c]]$.
            Thus $g(v) \in x \setminus h(c)$.
            We have $g(v) \in x \setminus c$.
            Therefore we can take $u \in x \setminus c$ such that $G(u) = v$.
            Then $v = H(u)$.
          End.
        End.

        (5) $H$ is injective.
        Indeed we can show that for all $u, v \in x$ if $u \neq v$ then
        $H(u) \neq H(v)$.
          Let $u,v \in x$.
          Assume $u \neq v$.

          Case $u,v \in c$.
            Then $H(u) = F(u)$ and $H(v) = F(v)$.
            We have $F(u) \neq F(v)$.
            Hence $H(u) \neq H(v)$.
          End.

          Case $u,v \notin c$.
            Then $H(u) = G(u)$ and $H(v) = G(v)$.
            We have $G(u) \neq G(v)$.
            Hence $H(u) \neq H(v)$.
          End.

          Case $u \in c$ and $v \notin c$.
            Then $H(u) = F(u)$ and $H(v) = G(v)$.
            Hence $v \in g[y \setminus f[c]]$.
            We have $G(v) \in y \setminus F[c]$.
            Thus $G(v) \neq F(u)$.
          End.

          Case $u \notin c$ and $v \in c$.
            Then $H(u) = G(u)$ and $H(v) = F(v)$.
            Hence $u \in g[y \setminus f[c]]$.
            We have $G(u) \in y \setminus f[c]$.
            Thus $G(u) \neq F(v)$.
          End.
        End.

        Consequently $H$ is a bijection between $x$ and $y$ (by 4, 5).
        Therefore $x$ and $y$ are equinumerous.
      End.
    \end{proof}
  \end{forthel}
\end{document}
