Logic issues in the construction of the transfinite sequence of subcomplexes $K^\bullet_\alpha$. Cases (1) and (3) are independent of previous steps, but it seems (2) is not: it requires to make a choice since $N_\alpha^\bullet$ is not unique. Instead of transfinite recursion on $\alpha$, maybe what one actually needs is the generalized axiom of dependent choices? Let $\kappa$ be an aleph. This axiom says:

> $\mathsf{DC}_\kappa$ [1, Sect. 8.1]. Let $S$ be a nonempty set and let $R$ be a binary relation such that for every $\alpha<\kappa$ and every $\alpha$-sequence $s=\left\langle x_{\xi}: \xi<\alpha\right\rangle$ of elements of $S$ there exists $y \in S$ such that $sRy$. Then there is a function $f: \kappa \rightarrow S$ such that for every $\alpha<\kappa,(f \mid \alpha) R f(\alpha)$.

(One has $\mathsf{AC}\Leftrightarrow\forall\kappa,\mathsf{DC}_\kappa$ [1, Theorem 8.1].)

The axioms $\mathsf{DC}_\kappa$ alone do not provide a transfinite sequence indexed on the class of all ordinals, but rather a transfinite sequence of length equal to an aleph. However, for our proof it suffices to consider some cardinal $\kappa$ greater than $\prod_{i\in\mathbb{Z}}|M^i|$ (as it is hinted in [#9511](https://stacks.math.columbia.edu/tag/079L#comment-9511), 4).

A disclaimer: All set theory I know I have learnt it in the last month, from scratch. I hadn't ever been into any kind of foundations of math, logical or set-theoretic ones.

### References ###

1. T. Jech, *The Axiom of Choice*