I went over the proof of Baire's Theorem for complete metric spaces (that a countable union of closed sets with empty interior has empty interior). In the proof, a decreasing nested sequence of closed balls is constructed. Then we choose a particular point from each of these balls and construct a sequence of those points.
I thought that we used axiom of choice when we chose these points. But then I read in multiple source that we actually don't use axiom of choice and that we use a weaker form, called the axiom of dependent choice. I looked up the definition of dependent choice:
Axiom of dependent choice (DC): Let $A$ be a non-empty set and $R \subseteq A \times A$ satisfy $\forall a \in A \; \exists b \in A: a R b$. Then there exists a sequence $(a_n)_n$ such that $a_n \; R \; a_{n+1} \; \forall n$.
The problem I have with this is that I don't understand how this axiom was used. First of all, what is the set $A$ and relation $R$ when we apply DC to prove Baire's Theorem? And secondly, could someone explain in some more details how this axiom is used.