Are we using the axiom of choice when we utilize a theorem a countable number of times?

Question

Lets say I have a sequence $(V_n)$ of open sets and a sequence $(K_n)$ of compact sets. For each pair $(V_n,K_n)$, Urysohn's lemma gives a function $f_n$ with some nice properties.

My question is: in order to form a sequence $(f_n)$ of functions I have to use the axiom of countable choice?

I can imagine arguing that Urysohn's lemma only gives me the information that the set $\{f_n\:|\: f_n\text{ satisfies a 'nice' property}\}$ is non-empty. But in order to actually have a function, I am doing a choice.

Also, I can imagine that Urysohn's lemma actually gives me a function, and so no choice is needed.

What argument is right?

Answer 1

Urysohn's lemma itself requires the Axiom of (Dependent) Choice.

However, once you have chosen the functions, the axiom of replacement tells you that your collection of functions is a set without the need for choice. And the function $\Bbb N\to \{f_n\}$ that makes it a sequence also doesn't require choice to be constructed.