Effective metacompactness for discrete metric spaces implies AC

Let $\mathcal{F}$ be an arbitrary family of nonempty sets and let $X:=(\mathcal{F}\times \{0\})\cup (\bigcup \mathcal{F}\times \{1\})$ carry the discrete metric; the two tags keep the family and its members apart, so that the zero-tagged family member is uniquely recovered from each cover pair. Explicitly, $d(u,v)=0$ if $u=v$ and $1$ otherwise satisfies separation and symmetry; if $u\mathrm{\ne }w$, at least one of $u\mathrm{\ne }v$ or $v\mathrm{\ne }w$ holds, proving the triangle inequality. Each radius-$1\mathrm{/}2$ ball is a singleton, so every subset is open. No disjointness of the members of $\mathcal{F}$ is used.

The family $\mathcal{U}$ of [F2] is an open cover of $X$ by [F2], so by the hypothesis applied once to this cover there are a point-finite open refinement $\mathcal{V}$ which covers $X$ and a map $a:\mathcal{V}\to \mathcal{U}$ with $V\subseteq a(V)$ for all $V\in \mathcal{V}$; no global refinement operator is assumed, only this one per-cover existential pair.

For each $F\in \mathcal{F}$ let $C(F):=\{V\in \mathcal{V}:(F,0)\in V\}$, the set of refinement members through the point $(F,0)$ of the space; $C(F)$ is nonempty because $\mathcal{V}$ covers $X$, and finite because $\mathcal{V}$ is point-finite at $(F,0)$.

Define $f(F):=\{x\in F:a(V)=\{(x,1),(F,0)\}\text{ for some }V\in C(F)\}$; then each $V\in C(F)$ determines a unique $x$ by its image pair (the one-tagged point); thus $f(F)$ is the image of the finite set $C(F)$ under a uniquely defined function. It is a finite subset of $F$, and it is nonempty because for $V\in C(F)$ one has $(F,0)\in V\subseteq a(V)$ and $a(V)\in \mathcal{U}$, so $a(V)=\{(x,1),(F^{\mathrm{\prime }},0)\}$ with $x\in F^{\mathrm{\prime }}\in \mathcal{F}$; now $(F,0)\in a(V)$ forces $(F,0)=(F^{\mathrm{\prime }},0)$, that is $F^{\mathrm{\prime }}=F$, because the alternative $(F,0)=(x,1)$ would give $0=1$. Hence $a(V)=\{(x,1),(F,0)\}$ with $x\in F$, as required.

The assignment $F\mapsto f(F)$ is therefore a function on the family $\mathcal{F}$ of nonempty sets whose values are nonempty finite subsets, which is Multiple Choice for $\mathcal{F}$, including the empty family via the empty function. For any indexed family $(X_i{)}_{i\in I}$ apply this construction to its set of values $\mathcal{F}=\{X_i:i\in I\}$ and compose to get $i\mapsto f(X_i)$; repeated values cause no difficulty. Since the original family was arbitrary, MC holds, and by [F1] the Axiom of Choice holds.