Compact CW images have finite cell support without choice

The image $L$ is compact in the open-cover sense. Indeed, the inverse images of any open cover of $L$ cover $K$; a finite subcover of $K$ yields a finite subcover of $L$ by the same covering members. This argument does not impose a metric on the target. Since $X$ is Hausdorff, [F2] makes $L$ closed in $X$.

Every nonempty compact subset $T\subseteq {\mathbb{R}}^d$ has a uniquely specified lexicographically least point. For $d\ge 1$, minimize its first coordinate using [F5] and restrict to the minimum level set. That set is nonempty, closed in $T$ and compact by [F3]. Minimize the next coordinate on it and continue through the finite ordered coordinate set. After $d$ steps all coordinates are fixed, and the nonempty final set is a singleton. Each minimum value and each level set is unique; no minimizing point is selected until the final singleton. For $d=0$, the sole possible nonempty subset of ${\mathbb{R}}^0$ is already a singleton. This is a finite prescription defined for every such $T$, not a family of arbitrary existential choices.

Let $e$ be a positive-dimensional open cell meeting $L$, with characteristic map ${\chi }_e:D^d\to X$. For $r\ge 0$ let $B_{d,r}$ be the concentric closed ball of radius $1-1\mathrm{/}(r+2)$ in $D^d$. These balls exhaust its interior. Thus some $B_{d,r}$ meets ${\chi }_e^{-1}(L)$; let $r_e$ be the least such integer. The set $T_e=B_{d,r_e}\cap {\chi }_e^{-1}(L)$ is a nonempty compact subset of ${\mathbb{R}}^d$: it is closed in the compact ball by step 1.1, continuity and [F3], [F4]. Let $v_e$ be its uniquely specified point from step 1.2 and set $x_e={\chi }_e(v_e)\in L\cap e$. For an occupied zero-cell use that point itself. The least integer, the finite sequence of coordinate minima, and the supplied characteristic map specify $x_e$ uniquely for every occupied cell; the resulting function is defined by this formula on the set of occupied cells.

Put $S=\{x_e:e\cap L\mathrm{\ne }\mathrm{\varnothing }\}$. Distinct occupied cells give distinct points, since their interiors are disjoint. For every subset $T\subseteq S$ and every closed cell $\bar{a}$, closure finiteness in [F1] says that $\bar{a}$ meets only finitely many open cells. Hence $T\cap \bar{a}$ is finite, with at most one point from each of those cells. A finite subset of a Hausdorff space is closed: singleton complements are open by the Hausdorff separation axiom, and finite unions of closed sets are closed. The weak topology in [F1] now makes $T$ closed in $X$. In particular $S$ is closed in $X$, hence closed in the compact $L$. By [F3], $S$ is compact.

For $s\in S$, the set $S\setminus \{s\}$ is closed in $X$ by step 3.1. Its complement intersects $S$ in $\{s\}$, so $S$ is discrete. Its singleton cover is an open cover of $S$ and therefore has a finite subcover. Thus $S$ is finite, without first extracting a countably infinite subset from an arbitrary infinite set. The bijection $e\mapsto x_e$ from occupied cells to $S$ shows that only finitely many cells meet $L$.

If there are occupied cells, start with their finite set. Add every cell meeting the boundary of a cell already in the set, and repeat downward in dimension. At each stage only finitely many cells are added by closure finiteness [F1]. A cell boundary lies in the preceding skeleton, so the dimensions strictly decrease along every newly required boundary chain. The finite starting set has a maximum dimension $N$, and after at most $N$ such downward stages no more are required. The union of these cells contains the entire closure of each member, hence is a finite CW subcomplex by [F1]. It contains $L$, because every point of $L$ belongs to an occupied open cell.

If $K$ or $L$ is empty, the empty subcomplex suffices and no minima are taken. For a point image, the closure process starts at its one occupied cell; it need not itself be a zero-cell. Zero-dimensional cells and the zero-dimensional Euclidean coordinate space were handled without a norm or empty-coordinate minimum. The radii in step 2.1 are strictly between zero and one and approach one, so all chosen preimages lie in cell interiors and no boundary point is mistaken for a point of that open cell. Nonregular characteristic maps cause no problem, since only their interior restrictions are used for the selected points. Steps 1.2 and 2.1 specify every selection uniquely, while steps 4.1 and 5.1 use compactness and finite closure operations; no AC is used anywhere.