Axiom of dependent choice and a problem about metric spaces In a homework assignment on metric spaces, there was a question stated like this:

Let $(X,d)$ be a metric space, and $S$,$T$ be subsets of $X$ (I suppose they are nonempty).
  If $S$ is compact, show that there exists $x\in S$ such that $d(x,T)=d(S,T)$, where $d(x,T):=\inf\{d(x,t):t\in T\}$ and $d(S,T):=\inf\{d(s,t):s\in S\land t\in T\}$.

I have already solved the problem, but there is a step that I used something I don't understand.
I assumed that $S$ is infinite (or else there are just finitely many points to choose from) and that, for contradiction, there is no point $x$ in $S$ satisfying the condition (so that the following construction is valid). Then, I have picked out points in $S$ according to the following rules:

First, pick $s_1\in S$ such that $d(S,T)\lt d(s_1,T)\lt d(S,T)+1$. Then, for every $n\in\Bbb N_{\ge 2}$, pick $s_n\in S$ such that $d(S,T)\lt d(s_1,T)\lt d(S,T)+\frac{1}{n}$ and $d(s_n,T)\lt d(s_{n-1},T)$.

I have heard that doing this repeated construction of points requires the  axiom of dependent choice. Is this the case? If so, how is the axiom of dependent choice involved? Please note that the axiom was not mentioned in the lectures, so please explain in detail how the axiom works.
 A: Your choice use recursion over the natural numbers (a countable set),
and as each choice depends upon the previous this means using the  Axiom of dependent choice (DC).
It is sufficient to use only the Axiom of countable choice (AC${}_\omega$) (strictly weaker than the DC) by for each $n\geq 1$ choosing $s_n$ so that $d(s_n,T)<d(S,T)+1/n$.  Such $s_n$ exists by the very definition of $d(S,T)$. 
After having constructed this sequence  you should use compactness, but this you probably already know.
A: Yes, your proof as stated does use the axiom of dependent choice, which is fine. Put informally, this axiom just states that the construction of the sequence $(s_i : i \in \mathbb{N})$ is valid. This sort of construction is used all the time, but in the context of formal set theory an axiom is required to state that it can be done.
There is another way to prove the result, though, which does not use the axiom of choice. Here is a sketch. Suppose the result fails. For each $n \in \mathbb{N}$, let $$U_n = \{ z \in S: d(z, T) > d(S,T) + 1/n\}.$$ Then each $U_n$ is open in $S$, and $S = \bigcup_{n \in \mathbb{N}} U_n$. But the cover $(U_n : n \in \mathbb{N})$ has no finite subcover, which means that $S$ is not compact, which is a contradiction.
That method of using compactness defines the entire cover $(U_n : n \in \mathbb{N})$ at once; there is no inductive sequence of choices made. As you get familiar with using compactness in that way, you can show that some other uses of the axiom of dependent choice can be replaced with more direct uses of compactness. 
A: The Principle of Dependent Choice essentially tells you that when you define a sequence by recursion, you don't need to specify exactly how the elements are chosen, but just that you can always continue your recursive assumptions. 
Here you don't specify which point is chosen. You just argue that there is a point satisfying the condition that you want. Dependent Choice is exactly what you need to ensure that indeed you have an actual sequence, and not just arbitrarily long finite sequences. 
