Intersection of nested sequence of non-empty compact sets is non-empty (using sequential compactness) Let $(X,d)$ be a metric space, and let $K_1, K_2, K_3, \ldots$ be a sequence of non-empty compact sets in this metric space such that $$K_1 \supseteq K_2 \supseteq K_3 \supseteq \cdots$$ Then the intersection $\bigcap_{n=1}^\infty K_n$ is non-empty. I am aware of the standard proof of this fact using covering compactness, but I am wondering if there is a proof that uses instead sequential compactness.
My attempt is the following. Since each $K_n$ is non-empty, we can pick some point $x_n \in K_n$ for each $n$ (this requires the axiom of choice). Now consider the sequence $(x_n)_{n=1}^\infty$. By the nesting property, we have $x_n \in K_1$ for each $n$. Since $K_1$ is compact, this means there is a convergent subsequence $(x_{n_j})_{j=1}^\infty$ which converges to a point $p \in K_1$. We will now show that in fact $p \in K_n$ for each $n$, which would prove that $p \in \bigcap_{n=1}^\infty K_n$ (hence, the intersection is non-empty). Let $n$ be arbitrary. We have $n_j \geq j$ so if $j \geq n$ then $n_j \geq n$. By the nesting property, this means that $x_{n_j} \in K_n$ for all $j \geq n$. Thus $(x_{n_j})_{j=n}^\infty$ is a sequence of points in $K_n$ which converges to $p$. Since $K_n$ is compact, it is closed, so $p \in K_n$.
It seems to me that the proof goes through, but all the proofs I could find online used covering compactness, which made me nervous that somehow using sequential compactness here doesn't work. I would be curious to hear if the proof above goes through (and if not, whether there is another way to use sequential compactness).

Your proof is indeed correct. As you noticed, it requires the axiom of choice, and that's perhaps the reason why it is avoided.
