The power set of $X$, denoted by $\powerset(X)$, is the unique set $Y$ such that
\[\forall y :\enspace y\in Y \enspace\lrimp\enspace y\subseteq X.\]The existence of $Y$ is justified by Axiom of Power Set and its uniqueness is justified by Axiom of Extensionality.
\[\powerset(\varnothing) = \{\varnothing\}.\]
PROP-P-CANT. Cantor’s Theorem.
For any $X$,
\[\lvert X\rvert < \lvert\powerset(X)\rvert.\]
Proof.If $f:X\to\powerset(X)$ were a surjection, there would be an $a\in X$ such that
\[f(a) = \{x\in X : x\notin f(x)\}.\]Consider whether $a\in f(a)$.
For any $X$,
\[\lvert\powerset(X)\rvert = 2^{\lvert X\rvert}.\]
Proof.
\[\varphi : \powerset(X)\to\fun(X,2), \, A\mapsto f_A\]is a bijection, where
\[f_A : X\to 2, \, x \mapsto \begin{cases} 1, & \text{if $x\in A$}; \\ 0, & \text{if $x\notin A$}. \end{cases}\]
PROP-P-CA. Corollary of Cantor’s Theorem + PROP-P-CARD
For any cardinal $\kappa$,
\[\kappa < 2^\kappa.\]