Cartan-Eilenberg injective resolutions exist

Put $B^p=\mathrm{im}{d}_K^{p-1}$, $Z^p=\ker d_K^p$ and $H^p=Z^p\mathrm{/}{B}^p$. The differential factors as $K^p\twoheadrightarrow B^{p+1}\rightarrowtail Z^{p+1}\rightarrowtail K^{p+1}$. Thus the two exact sequences to resolve are $0\to B^p\to Z^p\to H^p\to 0$ and $0\to Z^p\to K^p\to B^{p+1}\to 0$. At $p=b$, $B^b=0$.

Assemble resolutions $U^{p,\bullet }$ of $B^p$ and $V^{p,\bullet }$ of $H^p$ from successive injective embeddings of their cokernels, setting $U^{b,\bullet }=0$; F2 verifies the assembled complexes. For $0\to B^p\to Z^p\to H^p\to 0$, successive applications of the dual one-degree step F3 assemble $W^{p,\bullet }$ together with a degreewise split exact sequence $0\to U^{p,\bullet }\to W^{p,\bullet }\to V^{p,\bullet }\to 0$. Apply the same step to $0\to Z^p\to K^p\to B^{p+1}\to 0$ to assemble $I^{p,\bullet }$ in $0\to W^{p,\bullet }\to I^{p,\bullet }\to U^{p+1,\bullet }\to 0$. In the supplied-data branch, all embeddings and compatible next-degree lifts just named are part of the supplied successive choices. In the DC branch, they are selected from the nonempty sets supplied by enough injectives and F3, with the serial accounting given below.

Define $h:I^{p,\bullet }\to I^{p+1,\bullet }$ as projection onto $U^{p+1,\bullet }$ followed by inclusion into $W^{p+1,\bullet }$ and then $I^{p+1,\bullet }$. The next projection kills this image, so $h^2=0$. These arrows are cochain maps in the resolution direction, so $hv=vh$. Their kernels, images and cohomology objects in every vertical degree are respectively $W^{p,q}$, $U^{p+1,q}$ and $V^{p,q}$. Their augmentations are exactly the factorizations of $d_K$ in step 1.1. Every required term is injective and the two degreewise sequences split by the horseshoe construction.

Here is the countable-choice accounting for steps 2.1–3.1. Use three successive DC applications, each to a set of finite compatible states with an entire extension relation. In the first pass, enumerate the pairs $(p,q)$ with $p\ge b$, $q\ge 0$ and construct the side resolutions $U^{p,\bullet }$ and $V^{p,\bullet }$ one embedding at a time. At each task only the preceding vertical cokernel of that same side resolution is needed, so an order by increasing $p-b+q$, with the degree-$q-1$ task first, is serial by enough injectives and F2. The zero resolution $U^{b,\bullet }=0$ needs no selections. In the second pass all side resolutions are now available: enumerate $(p,q)$ again and use F3 successively in $q$ to construct $W^{p,\bullet }$ for $0\to B^p\to Z^p\to H^p\to 0$. In the third pass all $W^{p,\bullet }$ and $U^{p+1,\bullet }$ are available: enumerate $(p,q)$ and use F3 successively in $q$ to construct $I^{p,\bullet }$ for $0\to Z^p\to K^p\to B^{p+1}\to 0$. In each horseshoe pass, the degree-$q$ side terms are already fixed and the degree-$q-1$ middle cokernel is already constructed, so every finite state has a next extension. A fixed diagonal enumeration of each countable task set reaches every task; the unions of the three DC chains supply exactly the compatible data used in steps 2.1–3.1. Supplied successive choices give the same three passes in ZF. This does not select resolutions simultaneously for a proper class of complexes.

Set everything to zero for $p<b$ and $q<0$. Step 3.1 now verifies every clause of the Cartan–Eilenberg definition. For the zero complex one may take all data zero, and for a complex in one degree one may take its ordinary injective resolution in that column. Translating $p$ to $p-b$ yields nonnegative indices without an upper bound on $K$.