Avoid AC in the proof that compact subspaces of a Hausdorff space are closed. In Munkres Topology  Theorem 26.3 there is a proof that a compact subspace of a Hausdorff space is closed. The proof uses the axiom of choice (AC) at some point. Here we can find a proof by contradiction which avoids the AC. I was wondering if the following direct proof is also valid:
Let $Y$ be a compact subspace of the Hausdorff space $X$. We shall prove that $X-Y$ is open, so that $Y$ is closed.
Let $x_0$ be a point of $X-Y$. We show there is a neighborhood of $x_0$ that is disjoint from $Y$. Let $\mathcal{A}$ denote the collection of sets defined by
$$\mathcal{A}=\{V \text{ is an open neighborhood of some $y\in Y$ and }$$ $$ \text{there exists open neighborhood $U$ of $x_0$ such that $V\cap U=\emptyset$}\}$$
By the Hausdorff condition we have that $\mathcal{A} $ is open cover of $Y$, and since $Y$ is compact there exists a finite number of sets $V_1,\dots,V_n$ in $\mathcal{A}$ covering $Y$. For each $V_i$ we can choose an open neighborhood $U_i$ of $x_0$ such that $V_i\cap U_i=\emptyset$ (no AC needed since only finitely many choices). Then the open set $V_1\cup\dots\cup V_n$ contains $Y$ and is disjoint from the open neighborhood $U_1\cap\dots\cap U_n$ of $x_0$. Hence $U_1\cap\dots\cap U_n$ is the desired neighborhood of $x_0$.
To finish the proof without using AC we let $\mathcal{C}=\{U \text{ is an open neighborhood of some $x\in X-Y$ with $U\subset X-Y$}\}$. By the previous argument we have $X-Y=\cup \mathcal{C}$ so $X-Y$ is open.
Is this correct?
 A: Your proof is correct. However, you can also avoid to choose suitable $U_i$.
Since $X$ is Hausdorff, each $y \in Y$ has an open neighborhood $V$ such that $x_0 \notin \overline V$. Now consider the set $\mathcal A$ of all open neighborhoods $V$ of some $y  \in Y$ such that $x_0 \notin \overline V$. This is an open cover of $Y$, hence there exist finitely many $V_1,\ldots,V_n \in\mathcal A$ covering $Y$. We have
$$x_0 \notin \bigcup_i \overline V_i = \overline{\bigcup_i V_i} .$$
Hence
$$U(x_0) = X \setminus \overline{\bigcup_i V_i}$$
is an open neighborhood of $x_0$ contained in $X \setminus Y$.
Note that the existence of finite subcovers has nothing to do with AC, the definition of compactness assures it. In other words, compactness assures that you can make a very special choice: For each open cover you may select a finite subcover. This is a property which some spaces have and other spaces do not have. BUT: The choice of a finite subcover is not constructive, in concrete examples you may not explicitly know how to do it. In that sense it resembles AC. Moreover, in many cases you will need AC to prove that a certain space is compact. For example, arbitrary products of compact spaces are compact - and the proof requires AC.
