When do minimal subcovers always exist - without choice? In my answer to Doubt in the definition of a compact set, I sketched a proof of the following fact:

Suppose $X$ is a topological space such that every open cover of $X$ has a minimal subcover. Then $X$ is compact.

This is definitely not hard to prove, but the proof I gave uses the axiom "Every infinite set is Dedekind-infinite"$^*$ in a seemingly essential way. My question is, does this equivalence really require anything beyond ZF? If so, is there a good choiceless description of those spaces which have this "minimal subcover" property?

$^*$OK fine, my answer used full AC; but Henno Brandsma pointed out that the result is also proved in http://susanka.org/Notes/Topology.pdf, page 55, Exercise 17.1 using only this assumption. Susanka's proof is essentially the same, they just use a trick to bring down the choice needed.
 A: I claim that more than ZF is needed for this result.  Specifically, I claim that, in the basic Fraenkel model, the set $A$ of atoms with the discrete topology is a counterexample.  (I'm using a permutation model here, but the result transfers to ZF by the Jech-Sochor theorem.)  Of course, $A$ isn't compact because the cover by singletons has no finite subcover.  It remains to show that every cover $\mathcal U$ of $A$ (by arbitrary sets) has a minimal subcover.
Recall that $A$ is amorphous, i.e., every subset of it is finite or cofinite.  If $\mathcal U$ contains a cofinite set, then it has a finite subcover, from which we can extract a minimal subcover (e.g., as a subcover of smallest possible cardinality).  So assume from now on that $\mathcal U$ consists of finite sets.
Fix a finite support $E$ for $\mathcal U$, not necessarily a minimal support. Consider some element $a\in A-E$ and an element $X\in\mathcal U$ that contains $a$.  Without loss of generality, $X-\{a\}\subseteq E$, since $X$ is finite and we can just enlarge $E$.  (That's why I said "not necessarily minimal" above.) For each $b\in A-E$, let $X_b=(X-\{a\})\cup\{b\}$.  Since $E$ supports $\mathcal U$ and $X_a=X\in\mathcal U$, we have $X_b\in\mathcal U$ for every $b\in A-E$.  The family $\mathcal V=\{X_b:b\in A-E\}$ is a subfamily of $\mathcal U$ and covers all of $A$ except for the finite set $E-X$.  It's minimal with respect to this covering property, since each $b\in A-E$ is covered by just one element $X_b$ of $\mathcal V$. It remains only to take care of the exceptional points in $E-X$.
Adjoin to $\mathcal V$ finitely many additional sets from $\mathcal U$ to cover $E-X$.  Use as few additional sets as possible for this purpose.  Recall that these additional sets are finite, so they cover only finitely many points altogether and in particular only finitely many elements $b$ of $A-E$. Delete from $\mathcal V$ the corresponding finitely $X_b$'s.  The result of these modifications to $\mathcal V$ is a subfamily $\mathcal W$ of $\mathcal U$ (obviously) and covers $A$ because (1) elements of $E-X$ are covered by the additional sets adjoined to $\mathcal V$, (2) elements of $E\cap X$ are covered by the (infinitely many) $X_b$'s that we did not delete, and (3) elements $b$ of $A-E$ are covered by the corresponding $X_b$, which we did not delete unless that $b$ was also covered by one of the adjoined sets.
Finally, I claim that $\mathcal W$ is a minimal cover of $A$.  If you delete any of the surviving $X_b$'s, then the corresponding $b$ isn't covered.  If you delete any of the finitely many adjoined sets then you no longer cover all of $E-X$ since we used the smallest possible number of adjoined sets for that purpose.
