Existence of the cyclotomic $\mathbb Z_p$-extension of $\mathbb Q$

Let $p$ be an odd prime and $\overline{\mathbb Q}$ an algebraic closure of $\mathbb Q$. There is a subfield $\mathbb Q_\infty\subseteq\overline{\mathbb Q}$ such that $\mathbb Q_\infty/\mathbb Q$ is a $\mathbb Z_p$-extension, i.e. $\mathbb Q_\infty/\mathbb Q$ is Galois and

as topological groups (Krull topology on the left).

Concretely, $\mathbb Q_\infty$ is the unique subfield of $\mathbb Q(\mu_{p^\infty})$ fixed by the torsion subgroup $\mu_{p-1}\subset\mathbb Z_p^\times\cong\mathrm{Gal}(\mathbb Q(\mu_{p^\infty})/\mathbb Q)$: the cyclotomic $\mathbb Z_p$-extension of $\mathbb Q$. Composing with any number field $K$ it yields the cyclotomic $\mathbb Z_p$-extension of $K$, the basic object of Iwasawa theory.

Formalization Note "$\mathbb Z_p$-extension" is the platform definition IsZpExtension (Galois, with Galois group topologically isomorphic to Multiplicative ℤ_[p]).