\documentclass{article}

\usepackage{amsthm}
\usepackage{amssymb}

\usepackage{pstricks,pst-node}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}[theorem]{Definition}

\title{A Proof of Cantor-Bernstein-Schr\"oder}
\author{Chad E. Brown}

\begin{document}
\maketitle

We present a proof of Cantor-Bernstein-Schr\"oder based on Knaster's argument in~\cite{Knaster1928}.
The proof is given at a level of detail sufficient to prepare the reader to consider corresponding formal
proofs in interactive theorem provers.

\begin{definition}\label{monotone}
Let $\Phi:\wp(A)\to\wp(B)$. We say $\Phi$ is {\em{monotone}} if
$\Phi(U)\subseteq \Phi(V)$ forall $U,V\in\wp(A)$ such that $U\subseteq V$.
We say $\Phi$ is {\em{antimonotone}} if
$\Phi(V)\subseteq \Phi(U)$ forall $U,V\in\wp(A)$ such that $U\subseteq V$.
\end{definition}

\begin{definition}\label{setminus}
  For sets $A$ and $B$ we
  write $A\setminus B$ for $\{u\in A | u\notin B\}$.
\end{definition}

\begin{lemma}\label{setminusantimon}
  Let $A$ be a set and $\Phi:\wp(A)\to\wp(A)$ be
  given by $\Phi(X)= A\setminus X$.
  Then $\Phi$ is antimonotone.
\end{lemma}
\begin{proof}
  Left to reader.
\end{proof}

\begin{definition}\label{im}
  Let $f:A\to B$ be a function from a set $A$ to a set $B$.
  For $X\in \wp(A)$ we write $f(X)$ for $\{f(x) | x\in X\}$.
\end{definition}

\begin{lemma}\label{immon}
  Let $f:A\to B$ be a function from a set $A$ to a set $B$.
  Let $\Phi:\wp(A)\to\wp(B)$ be given by $\Phi(X) = f(X)$.
  Then $\Phi$ is monotone.
\end{lemma}
\begin{proof}
  Left to reader.
\end{proof}

\begin{theorem}[Knaster-Tarski Fixed Point]\label{kt}
  Let $\Phi:\wp(A)\to\wp(A)$.
  Assume $\Phi$ is monotone.
  Then there is some $Y\in\wp(A)$ such that $\Phi(Y)=Y$.
\end{theorem}
\begin{proof}
  Let $Y$ be $\{u\in A | \forall X\in\wp(A). \Phi(X)\subseteq X \to u\in X\}$.
  The following is easy to see:
  \begin{equation}
    Y\subseteq X {\mbox{~for~all~}} X\in\wp(A) {\mbox{~such~that~}} \Phi(X)\subseteq X. \label{fact1}
  \end{equation}
  We prove $\Phi(Y)\subseteq Y$ and $Y\subseteq\Phi(Y)$.

  We first prove $\Phi(Y)\subseteq Y$.
  Let $u\in\Phi(Y)$. We must prove $u\in Y$. Let $X\in\wp(A)$ such that $\Phi(X)\subseteq X$ be given.
  By ({\ref{fact1}}) $Y\subseteq X$. Hence $\Phi(Y)\subseteq\Phi(X)$ by monotonicity of $\Phi$.
  Since $u\in \Phi(Y)$, we have $u\in \Phi(X)$.
  Since $\Phi(X)\subseteq X$, we conclude $u\in X$.

  We next turn to $Y\subseteq\Phi(Y)$. 
  Since $\Phi(Y)\subseteq Y$, we know $\Phi(\Phi(Y))\subseteq \Phi(Y)$ by monotonicity of $\Phi$.
  Hence $Y\subseteq\Phi(Y)$ by ({\ref{fact1}}).
\end{proof}

\begin{definition}
  Let $f:A\to B$ be a function.
  We say $f$ is {\em{injective}} if $\forall xy\in A. f(x) = f(y) \to x = y$.
\end{definition}

\begin{definition}\label{eqpot}
  We say sets $A$ and $B$ are {\em{equipotent}} if there exists a relation $R$ such that
  \begin{enumerate}
  \item $\forall x\in A.\exists y\in B. (x,y)\in R$
  \item $\forall y\in B.\exists x\in A. (x,y)\in R$
  \item $\forall x\in A.\forall y\in B.\forall z\in A.\forall w\in B.(x,y)\in R \land (z,w)\in R \to (x=z \iff y=w)$
  \end{enumerate}
\end{definition}

\begin{theorem}[Cantor-Bernstein-Schr\"oder]\label{cbs}
  If $f:A\to B$ and $g:B\to A$ are injective,
  then $A$ and $B$ are equipotent.
\end{theorem}
\begin{proof}
  Let $f:A\to B$ and $g:B\to A$ be given injective functions.
  Let $\Phi:\wp(A)\to\wp(A)$ be defined by $\Phi(X) = g(B\setminus f(A\setminus X))$.
  It is easy to see that $\Phi$ is monotone by Lemmas~\ref{setminusantimon} and~\ref{immon}.
  By Theorem~\ref{kt} there is some $C\in\wp(A)$ such that $\Phi(C) = C$.
  Hence $C\subseteq A$ and
  \begin{equation}
    \forall x.x\in C\iff x\in g(B\setminus f(A\setminus C)). \label{fact2}
  \end{equation}
  We can visualize the given information as follows:
  \begin{center}
    \begin{pspicture}(9,4)
      \pscircle[linewidth=2pt](2,2){1.5}
      \pscircle[linewidth=2pt](7,2){1.5}
      \rput(0.6,3.2){$A$}
      \rput(2,2.5){$A\setminus C$}
      \rput(2,1.5){$C$}
      \rput(8.4,3.2){$B$}
      \rput(7,2.5){$f(A\setminus C)$}
      \rput(7,1.5){$B\setminus f(A\setminus C)$}
      \rput(2,2){\rnode{A}{}}
      \rput(7,2){\rnode{B}{}}
      \psline{-}(0.5,2)(3.5,2)
      \psline{-}(5.5,2)(8.5,2)
      \psset{nodesep=44pt}
      \ncarc{->}{A}{B}\aput(0.5){$f$}
      \ncarc{->}{B}{A}\aput(0.5){$g$}
    \end{pspicture}
  \end{center}

  Let $R = \{(x,y)\in A\times B| x\notin C \land y = f(x) \lor x\in C \land x = g(y)\}$.
  We must prove the three conditions in Definition~\ref{eqpot}.
  \begin{enumerate}
  \item Let $x\in A$ be given. We must find some $y\in B$ such that $(x,y)\in R$.
    We consider cases based on whether $x\in C$ or $x\notin C$.
    If $x\notin C$, then we can take $y$ to be $f(x)$.
    Assume $x\in C$.
    By ({\ref{fact2}}) we know $x\in g(B\setminus f(A\setminus C))$.
    Hence there is some $y\in B\setminus f(A\setminus C)$ such that $x=g(y)$
    and we can use this $y$ as the witness.
  \item Let $y\in B$ be given. We must find some $x\in A$ such that $(x,y)\in R$.
    We consider cases based on whether or not $y\in f(A\setminus C)$.
    If $y\in f(A\setminus C)$, then there is some $x\in A\setminus C$ such that $f(x)=y$ and we can use this same $x$ as the witness.
    Assume $y\notin f(A\setminus C)$.
    Note that $g(y)\in C$ using {\ref{fact2}} and $y\in B\setminus f(A\setminus C)$.
    Hence we can take $g(y)$ as the witness.
  \item Before proving the third property, we prove the following claim:
    \begin{equation}
      \forall x\in A.\forall y \in B. x\in C \land x = g(y) \to y\notin f(A\setminus C)
      \label{fact3}
    \end{equation}
    Let $x\in A$ and $y\in B$ be given. Assume $x\in C$, $x=g(y)$ and $y\in f(A\setminus C)$.
    Since $x\in C$,there is some $w\in B\setminus f(A\setminus C)$ such that $g(w)=x$ by (\ref{fact2}).
    Since $g$ is injective, $w=y$ contradicting $y\in f(A\setminus C)$.
    
    Now that we know (\ref{fact3}) we can easily prove the third property by splitting into four cases.
    Let $x\in A$, $y\in B$, $z\in A$ and $w\in B$ be given. Assume $(x,y)\in R$ and $(z,w)\in R$.
    By the definition of $R$ there are two cases for $(x,y)\in R$ and two cases for $(z,w)\in R$.
    In each case we need to prove $x=z\iff y=w$.
    \begin{itemize}
    \item Assume $x\notin C$, $y=f(x)$, $z\notin C$ and $w=f(z)$.
      The fact that $x=z\iff y=w$ follows easily from injectivity of $f$.
    \item Assume $x\notin C$, $y=f(x)$, $z\in C$ and $z=g(w)$.
      In order to prove $x=z\iff y = w$ we argue that $x\not=z$ and $y\not=w$.
      Clearly $x\not= z$ since $x\notin C$ and $z\in C$.
      By (\ref{fact3}) we know $w\notin f(A\setminus C)$.
      On the other hand $y\in f(A\setminus C)$ since $y=f(x)$ and $x\in A\setminus C$.
      Hence $y\not=w$.
    \item Assume $x\in C$, $x=g(y)$, $z\notin C$ and $w=f(z)$.
      Again in order to prove $x=z\iff y = w$ we argue that $x\not=z$ and $y\not=w$.
      Clearly $x\not= z$ since $x\in C$ and $z\notin C$.
      By (\ref{fact3}) we know $y\notin f(A\setminus C)$.
      On the other hand $w\in f(A\setminus C)$ since $w=f(z)$ and $z\in A\setminus C$.
      Hence $y\not=w$.
    \item Assume $x\in C$, $x=g(y)$, $z\in C$ and $z=g(w)$.
      The fact that $x=z\iff y=w$ follows easily from injectivity of $g$.
    \end{itemize}
  \end{enumerate}
\end{proof}

\begin{corollary}
  If $f:A\to B$ is injective and $B\subseteq A$,
  then $A$ and $B$ are equipotent.
\end{corollary}
\begin{proof}
  This follows immediately from Theorem~\ref{cbs} using the injection from $B$ into $A$,
  since this injection is obviously injective.
\end{proof}

\bibliographystyle{plain}
\bibliography{refs}

\end{document}
