$\aleph_1 \le 2^{\aleph_0}$ under the Axiom of Choice, because $2^{\aleph_0}$ is a cardinal strictly above $\aleph_0$ and $\aleph_1$ is the least such; so $\omega_1$ injects into $\mathbb{R}$

Assume the Axiom of Choice (The Axiom of Choice). Then

$\aleph_0 < \aleph_1 \le 2^{\aleph_0},$

and consequently $\omega_1$ injects into $\mathbb{R}$ (The first uncountable ordinal $\omega_1 := \aleph(\omega)$, $\mathbb{R} \approx \mathcal{P}(\mathbb{N})$ in ZF, by the Cantor set for one injection and by the cuts $\{q \in \mathbb{Q} : q < x\}$ for the other; so $\lvert \mathbb{R} \rvert = 2^{\aleph_0}$ under the Axiom of Choice). Moreover $2^{\aleph_0} = \aleph_\alpha$ for exactly one ordinal $\alpha$, and that $\alpha$ satisfies $1 \le \alpha$ (Every infinite cardinal is $\aleph_\alpha$ for exactly one ordinal $\alpha$, in ZF; and, assuming the Axiom of Choice, every infinite set is equinumerous with exactly one aleph).

The computation is one line and uses nothing about $\mathbb{R}$: $2^{\aleph_0}$ is a cardinal strictly above $\aleph_0$ by Cantor's theorem in cardinal form (Assuming the Axiom of Choice, $2^{\kappa} = \lvert \mathcal{P}(\kappa) \rvert$, and Cantor's theorem in cardinal form: $\kappa < 2^{\kappa}$), and $\aleph_1$ is by construction the least cardinal strictly above $\aleph_0$ (For every set $A$ the Hartogs number $\aleph(A)$ is a cardinal, and for every cardinal $\kappa$ it is the least cardinal strictly above $\kappa$; this is a theorem of ZF). The inequality is therefore forced, and the interest lies entirely in the fact that nothing here decides whether it is an equality.

What the inequality is not. It is not evidence for the continuum hypothesis, and it is not a partial result towards one. $\aleph_1 \le 2^{\aleph_0}$ holds in every model of ZFC, including those where $2^{\aleph_0}$ is very large; the inequality is a consequence of $\aleph_1$ being defined as a least cardinal above $\aleph_0$, so it would hold even if the continuum were enormous.

Where the real constraint lies. The one genuine restriction on $2^{\aleph_0}$ proved in this development is on its cofinality, not on its position: Assuming the Axiom of Choice: $\kappa < \kappa^{\operatorname{cf}(\kappa)}$ for every infinite cardinal $\kappa$, and $\operatorname{cf}(2^{\kappa}) > \kappa$; in particular $\operatorname{cf}(2^{\aleph_0}) > \aleph_0$ gives $\operatorname{cf}(2^{\aleph_0}) > \aleph_0$, which excludes candidate values such as $\aleph_\omega$ (FALSE: $2^{\aleph_0} = \aleph_\omega$) while excluding neither $\aleph_1$ nor $\aleph_2$, both of which are regular under choice. Whether $2^{\aleph_0} = \aleph_1$ is the continuum hypothesis, and What each result on this page costs in choice, and where the continuum escapes what ZFC can decide records what is and is not settled about it here.

Without choice the statement is not even expressible in this form. In ZF alone $\mathcal{P}(\mathbb{N})$ need not be well-orderable, so $2^{\aleph_0}$ need not be a cardinal and "$\aleph_1 \le 2^{\aleph_0}$" has no ordinal to compare. What is a theorem of ZF is the existence of $\omega_1$ itself (The first uncountable ordinal $\omega_1 := \aleph(\omega)$, $\omega_1$ is uncountable, every ordinal below it is at most countable, it is a cardinal and a limit ordinal, and its existence is a theorem of ZF); the injection $\omega_1 \to \mathbb{R}$ of step 2.1 is obtained here from the Axiom of Choice, and nothing above claims it without that hypothesis.