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).
