Under choice, every open cover of a metric space has a point-finite open refinement

Well order $\{C_{\alpha }\}$ by [A1], and write $R(x,n)=B(x,2^{-n})$. A ball $R(z,n+1)$ is chosen for $C_{\alpha }$ when $n$ is the least natural number with $R(z,n)\subseteq C_{\alpha }$ and, in addition, $R(z,n)\subseteq C_{\beta }$ for some $\beta <\alpha$. Let ${\mathcal{G}}_{\alpha }$ be the union of all balls chosen for $C_{\alpha }$.

Put $C_{\alpha }^{\mathrm{\prime }}:=C_{\alpha }\setminus \overline{{\mathcal{G}}_{\alpha }}$. Each $C_{\alpha }^{\mathrm{\prime }}$ is open and refines $C_{\alpha }$.

The $C_{\alpha }^{\mathrm{\prime }}$ cover. Otherwise let $C_{\alpha }$ be the first original member containing an omitted point $x$. Then $x\in \overline{{\mathcal{G}}_{\alpha }}$. By [L1], choose $N$ with $B(x,3\cdot 2^{-N})\subseteq C_{\alpha }$, and put $\delta =2^{-(N+2)}$. Some chosen ball $R(z,n_z+1)$ meets $B(x,\delta )$; write its radius as $r=2^{-(n_z+1)}$. If $r>\delta$, then $d(x,z)<r+\delta <2r$, so its expanded ball $R(z,n_z)$ contains $x$. If $r\le \delta$, then $d(x,z)<r+\delta \le 2\delta <2^{-N}$, so $R(z,N)\subseteq C_{\alpha }$ and minimality gives $n_z\le N$; hence $r\ge 2^{-(N+1)}=2\delta$, a contradiction. Thus in every case an expanded chosen ball contains $x$. That expanded ball lies in some $C_{\beta }$ with $\beta <\alpha$, contradicting the choice of $\alpha$.

If $x\in C_{\alpha }^{\mathrm{\prime }}$ and $n$ is least with $R(x,n)\subseteq C_{\alpha }$ (which exists by [L1]), then $C_{\alpha }$ is the first cover member containing $R(x,n)$: otherwise $R(x,n+1)$ would be chosen for $C_{\alpha }$ and would contain $x$, contrary to $x\mathrm{\notin }\overline{{\mathcal{G}}_{\alpha }}$. For each $n$ there is at most one such first member, and as $n$ increases their ordinal indices are nonincreasing. Infinitely many distinct indices would therefore give an infinite strictly descending sequence of ordinals, impossible because its range has a least member. Thus only finitely many $C_{\alpha }^{\mathrm{\prime }}$ contain $x$.

Thus $\{C_{\alpha }^{\mathrm{\prime }}\}$ is the point-finite open refinement required by [F2].