\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{../lib/tex/naproche}

\title{Cantor's Theorem}
\author{}
\date{}

\setlength{\parindent}{0em}

\begin{document}
  \pagenumbering{gobble}

  \maketitle

  In this document we give a proof of Cantor's Theorem:

  \begin{theorem*}
    There is no surjection from a set onto its powerset.
  \end{theorem*}

  Some basic notions and set-theoretic axioms used to formulate and prove it are
  taken from:

  \begin{forthel}
    [readtex \path{preliminaries.ftl.tex}]
  \end{forthel}

  Moreover, we need to provide certain definitions concerning surjective
  functions and the notion of powerset.

  \begin{forthel}
    \begin{definition*}
      Let $X$ be a set.
      A function of $X$ is a function $f$ such that $\dom(f) = X$.
    \end{definition*}

    \begin{definition*}
      Let $f$ be a function and $Y$ be a set.
      $f$ surjects onto $Y$ iff $Y = \class{f(x) | x \in \dom(f)}$.
    \end{definition*}

    Let a surjective function from $X$ to $Y$ stand for a function of $X$ that
    surjects onto $Y$.

    \begin{definition*}
      Let $X$ be a set.
      The powerset of $X$ is the collection of subsets of $X$.
    \end{definition*}

    \begin{axiom*}
      The powerset of any set is a set.
    \end{axiom*}
  \end{forthel}

  On this basis Cantor's theorem and its proof can be formalized as follows.

  \begin{forthel}
    \begin{theorem*}[Cantor]
      Let $M$ be a set.
      No function of $M$ surjects onto the powerset of $M$.
    \end{theorem*}
    \begin{proof}
      Assume the contrary.
      Take a surjective function $f$ from $M$ to the powerset of $M$.
      The value of $f$ at any element of $M$ is a set.
      Define \[ N = \class{x \in M | \text{$x$ is not an element of $f(x)$}}. \]
      $N$ is a subset of $M$.
      Consider an element $z$ of $M$ such that $f(z) = N$.
      Then \[ z \in N \iff z \notin f(z) = N. \]
      Contradiction.
    \end{proof}
  \end{forthel}
\end{document}
