\import{set/powerset.tex}
\import{function.tex}

\subsection{Cantor's theorem}


\begin{theorem}[Cantor]\label{cantor}
    There exists no surjection from $A$ to $\pow{A}$.
\end{theorem}
\begin{proof}
    Assume there exists a surjection from $A$ to $\pow{A}$.
    Take $f$ such that $f$ is a surjection from $A$ to $\pow{A}$ by assumption.
    Let $B = \{a \in A \mid a\notin f(a)\}$.
    We have $B\subseteq A$ by \cref{subseteq}.
    Thus $B\in\pow{A}$ by \cref{pow_iff}.
    Take $a'$ such that $a'\in A$ and $f(a') = B$ by \cref{surj}.
    We have if $a'\in B$, then $a'\notin B$ by assumption.
    We have if $a'\notin B$, then $a'\in B$ by assumption.
    Contradiction by assumption.
\end{proof}