This is the usual definition of a compact space: A topological space is compact iff every open cover has a finite subcover.
It is possible to consider only covers by sets from a fixed base $\mathcal B$ instead of arbitrary cover. So we have the following result:
Claim. Let $\mathcal B$ be a base for $X$. Let $X$ be a space such that every open cover with sets from $\mathcal B$ has a finite subcover. Then $X$ is compact.
The same claim is true also for a subbase. In this case it is known as Alexander subbase theorem. The usual proof uses Zorn's Lemma and it cannot be proven in ZF alone. It is equivalent to the Boolean prime ideal theorem and the Ultrafilter lemma.1
If we only work with bases, the proof of the above claim is much more straightforward – still it uses Axiom of Choice:
Proof. Let $\mathcal U$ by any open cover of $X$. Let us take the set $\mathcal B'=\{B\in\mathcal B; (\exists U\in\mathcal U) B\subseteq U\}$, i.e., the set consisting of all basic set which lie entirely inside some set from the original open cover. The set $\mathcal B'$ is an open cover of $X$. (Indeed, for every $x\in X$ there is some $U\in\mathcal U$ such that $x\in U$. And, by the definition of base, there exists $B\in\mathcal B$ with $x\in B\subseteq U$.)
Since $\mathcal B'\subseteq\mathcal B$, there is an open subcover $\{B_1,\dots,B_n\}$ of $\mathcal B'$. Now for each $B_i$, $i=1,\dots,n$ we can choose some $U_i\in\mathcal U$ such that $B_i\subseteq U_i$. The set $\{U_1,\dots,U_n\}$ is a finite subcover of $\mathcal U$. Q.E.D
Question. Can the above claim be shown in ZF?
1I can add another reference if I find it, but at least this is claimed in some posts on this site, such as: Ultrafilter Lemma and Alexander subbase theorem and What is Alexander subbase theorem equivalent to?
Best Answer
The proof for basic covers can be written choiceless, as you did:
$\mathcal{B}'=\{B \in \mathcal{B}: \exists U \in \mathcal{U}: B \subseteq U\}$ is a well-defined family of sets (no choice needed).
It is a cover of $X$ because $\mathcal{U}$ is and $\mathcal{B}$ is a base: let $X \in X$. For some $U_x \in \mathcal{U}$ we have $x \in U_x$. There is a basic $B_x \in \mathcal{B}$ such that $x \in B_x \subseteq U_x$. Now the existence of $U_x$ "witnesses" that $B_x \in \mathcal{B}'$ and that set contains $x$. As $x$ was arbitrary, $\mathcal{B}'$ is a cover of $X$ by base elements.
By assumption, this has a finite subcover $\{B_1,\ldots, B_n\} \subseteq \mathcal{B}'$, for each $1 \le i\le n$ pick a "witnessing" $U_i \in \mathcal{U}$ with $B_i \subseteq U_i$ (we don't need AC for finitely many choices (see e.g. this answer). And the larger $U_i$ of course also form a cover of $X$ and are the required subcover of $\mathcal{U}$.
Another proof approach would use choice: Suppose $\mathcal{U}$ is an open cover. For each $x$ pick $U_x$ in the cover and a base element $B_x$ such that $x \in B_x \subseteq U_x$. The $\{B_x: x \in X\}$ form a cover of $X$ "by construction", so finitely many, say, $B_{x_1},\ldots, B_{x_n}$ cover $X$ and $\{U_{x_1}, \ldots, U_{x_n}\}$ is then a finite subcover of $\mathcal{U}$. Quick, easy but heavy on choice (which we don't really need for this implication, as we saw above). So the proof set-up matters. Very often, with smarter definitions, we can avoid some uses of AC. Most topologists "don't care", and arguments of the latter type are very common.
For the subbase version (Alexander's subbase lemma), we do essentially need a form of choice: the standard reference book Consequences of the axiom of choice mentions it under subtype [14]: equivalent to the Boolean prime ideal theorem and also the theorem that any product of compact Hausdorff spaces is compact. (so "almost" full AC IMHO).