Solution (source code)

= Solution

For cardinals, $\kappa<\lambda$ means that there is an injection $\kappa\to\lambda$ but no bijection. Under the <axiom of choice>, every set is well-orderable, so every infinite cardinal is the initial ordinal $\aleph_\alpha$ for a unique ordinal $\alpha$. <Cantor diagonal argument>[Cantor theorem] gives
$$
\aleph_\alpha<2^{\aleph_\alpha},
$$
and minimality of the successor cardinal gives
$$
\aleph_{\alpha+1}\leq2^{\aleph_\alpha}.
$$
The strict inequality $\aleph_{\alpha+1}<2^{\aleph_\alpha}$ printed in the conversion is not provable and can be false under the generalized continuum hypothesis; the intended symbol must be $\leq$.