How much choice is necessary to prove this statement?

Question

Consider the following statement (in $\mathsf{ZF}+\text{AC}_\omega (\mathbb{R})$):

There exists $(\varphi_\alpha)_{\alpha\in\omega_1}$ with $\varphi_\alpha : \alpha \rightarrow \mathbb{N}^\mathbb{N}$ injective and $\text{ran}(\varphi_\alpha)$ is closed and $\text{rank}_{CB}(\text{ran}(\varphi_\alpha)) = 1$, i.e. $\text{ran}(\varphi_\alpha)$ is made of isolated points, for all $\alpha\in \omega_1$.

where $\mathbb{N}^\mathbb{N}$ is the Baire space (the space of infinite sequences of natural numbers with its usual topology) and $\text{rank}_{CB}$ is the Cantor-Bendixon rank. The statement trivially holds if we assume $\text{AC}_{\omega_1}$.
My questions are:

1. How much choice do we need (at least) to prove the above statement? Or more generally what known "weak" axiom (on top of $\mathsf{ZF}+\text{AC}_\omega (\mathbb{R})$) can be assumed to prove the statement?
2. Is it equivalent to the statement "There exists an $\omega_1$ subset of the reals"? In case it is not, is it consistent $\mathsf{ZF}+\text{AC}_\omega (\mathbb{R})+$ The above statement $+$ "It does not exists an $\omega_1$ subset of the reals"?

Thanks!

Answer 1

Your statement is equivalent to the assertion that there is a function choosing an enumeration of every countable ordinal. From an enumeration of $\alpha,$ you can easily inject it into a countable set of isolated points in Baire space. For the other direction, if $\varphi_{\alpha}$ injects $\alpha$ into Baire space, with the range a set of isolated points, there is a surjective partial map from basic open sets onto $\alpha,$ by sending $U \mapsto \beta$ if $\beta$ is unique such that $\varphi_{\alpha}(\beta) \in U.$ From this we can easily enumerate $\alpha.$ Note that by the Cantor-Bendixson analysis, any closed countable set of reals can be canonically enumerated, by sending basic open sets to the unique point in $U$ of maximal rank if there is such a point.

This principle implies there is an $\omega_1$-sequence of reals, since an enumeration of an ordinal can be canonically coded by a real. It is strictly stronger than the existence of an $\omega_1$-sequence of reals. For example, it clearly implies $\omega_1$ is regular, while in Figura's model ($\mathcal{M}36$ in Consequences of the Axiom of Choice), there is an $\omega_1$-sequence of reals yet $\omega_1$ is singular.

Note that everything above is purely in ZF. The possibility remains that countable choice for reals plus an $\omega_1$-sequence of reals implies your principle, though that seems unlikely. I would guess adding $\omega_1$ Cohen reals to the Solovay model would result in a model with an $\omega_1$-sequence of reals and DC but no choice of enumerations for every countable ordinal. I have not verified this however.