From Munkres' Topology book:
Theorem 48.2 (Baire category theorem). If $X$ is a compact Hausdorff space or a
complete metric space, then $X$ is a Baire space.
Proof. Given a countable collection $\{A_n\}$ of closed set of $X$ having empty interiors,
we want to show that their union $\cup A_n$ also has empty interior in $X$. So, given the
nonempty open set $U_0$ of $X$, we must find a point $x$ of $U_0$ that does not lie in any of
the sets $A_n$.
Consider the first set $A_1$. By hypothesis, $A_1$ does not contain $U_0$. Therefore, we
may choose a point $y$ of $U_0$ that is not in $A_1$. Regularity of $X$, along with the fact that
$A_1$ is closed, enables us to choose a neighborhood $U_1$ of $y$ such that
$$\bar{U}_1\cap A_1 = \emptyset$$
$$\bar{U}_1\subset U_0$$ If $X$ is metric, we also choose $U_1$ small enough that its diameter is less than $1$.
In general, given the nonempty open set $U_{n−1}$, we choose a point of $U_{n−1}$ that is
not in the closed set $A_n$, and then we choose $U_n$ to be a neighborhood of this point
such that
$$\bar{U}_n\cap A_n = \emptyset$$
$$\bar{U}_n\subset U_{n-1}$$
$$\text{diam } U_n <\frac{1}{n} \text{ in the metric case}$$
From there Munkres finishes the proof by showing that $\cap \bar{U}_n$ is nonempty.
This proof uses the axiom of dependent choice (DC), and I just want to make sure I correctly understand the details of how it is applied.
Axiom of dependent choice (DC). Let $S$ be a nonempty set and $R\subset S\times S$ such that for all $a\in S$ there exists $b\in S$ such that $(a,b)\in R$. Then there exists a sequence $(a_n)$ in $S$ such that $(a_n,a_{n+1})\in R$ for all $n$.
I believe the current form of the axiom is not directly applicable in the above proof. So I first prove a corollary:
Corollary. Let $B_1,B_2,\dots$ be a sequence of nonempty sets, and, for each $n$, let $R_n\subset B_n\times B_{n+1}$ be such that for all $b_n\in B_n$ there exists $b_{n+1}\in B_{n+1}$ such that $(b_n,b_{n+1})\in R_n$. Then there exists a sequence $(b_n)$ in $B_1\times B_2 \times \dots$ such that $(b_n,b_{n+1})\in R_n$ for each $n$.
Proof. Let $S_1=B_1$ and, for each $n>1$, let $S_n=\bigg\{(b_1,\dots,b_n)\in B_1\times\dots\times B_n: (b_k,b_{k+1})\in R_k, k=1,\dots,n-1\bigg\}$. Let $S=\cup S_n$ and let
$$R=\bigg\{\Big((b_1,\dots,b_n),(b_1,\dots,b_{n+1})\Big): (b_1,\dots,b_{n+1})\in S_{n+1} \text{ for some $n$}\bigg\}$$
Since $(b_1,\dots,b_{n+1})\in S_{n+1}$ implies $(b_1,\dots,b_{n})\in S_{n}$ we see that $R\subset S\times S$. Moreover our assumption about each $R_n$ implies that $S$ statisfies the assumption in DC with respect to $R$. Therefore DC gives us a sequence in $S$ of the form
$$(b_1,\dots,b_{n})$$
$$(b_1,\dots,b_{n+1})$$
$$\dots$$
for some $n$. Taking the sequence $(b_n)$ gives us the desired sequence.
Note that if $R_n=B_n\times B_{n+1}$ for each $n$ then the previous corollary gives the axiom of countable choice.
Now back to the proof in Munkres. I will apply the previous corollary with $B_1=\{U_1\}$ and $B_2=B_3=\dots=B$, where $B$ is the collection of all nonempty open subsets of $X$. For each $n$ let $$R_n=\bigg\{(U,V)\in B_n\times B_{n+1} : \bar{V}\cap A_{n+1} = \emptyset, \bar{V}\subset U, \text{diam } V <\frac{1}{n+1} \text{ in the metric case}\bigg\}$$
Then Munkres' proof shows that for all $n$ and each $b_n \in B_n$ there exists $b_{n+1} \in B_{n+1}$ such that $(b_n,b_{n+1})\in R_n$. We can therefore apply the previous corollary to obtain
the desired sequence of open sets $(U_n)$.
Is this the correct way to proceed? Thanks a lot for your help.
Best Answer
Well, the thing about Dependent Choice is that there's just so many ways to state it, and almost all of them are so naturally-sounding statements, that you can just ignore it and pretend it's how you'd always do math.
For example, one of the examples is a "generalised recursive principle", which is very similar to your corollary. My preferred equivalence is generally "every tree without maximal nodes contains an infinite chain", because it's often easy to describe your recursive construction as a tree (where the successor of each nodes are the optional choices for the next step).
But as you can prove it from $\sf DC$, you can also just "sort of embed that proof" into your proof. Namely, define a set $S$ and relation $R$ on that set.
In either case, your suggested way is absolutely fine.