Choice produces an undetermined natural-number game

Apply F2 using A1 and then F3 to obtain the infinite initial cardinal $\kappa =\mathrm{\mid }R\mathrm{\mid }$, a bijection $\kappa \to R$ and its induced well-order of $R$. Infinitude follows already from the distinct constant sequences. By F1 index I's strategies as ${\sigma }_{\alpha }$ and II's as ${\tau }_{\alpha }$, $\alpha <\kappa$. Each compatible-play set has cardinal $\kappa$ by that same fact.

Suppose pairs $(x_{\beta },y_{\beta })$ have been chosen for $\beta <\alpha <\kappa$. Their used set is the image of $\alpha \times 2$, so has cardinal at most $2\mathrm{\mid }\alpha \mathrm{\mid }$. For infinite $\alpha$, F3 gives $\mathrm{\mid }\alpha \mathrm{\mid }<\kappa$ by initiality, and F4 gives $2\mathrm{\mid }\alpha \mathrm{\mid }=\mathrm{\mid }\alpha \mathrm{\mid }<\kappa$; adding one further point still has that cardinal by F4. For finite $\alpha$, both the used set and its extension by one point are finite, hence smaller than infinite $\kappa$. Therefore some play compatible with ${\sigma }_{\alpha }$ is unused, and after selecting it some play compatible with ${\tau }_{\alpha }$ is still unused.

Set $x_{\alpha }$ to the least eligible ${\sigma }_{\alpha }$-play in the fixed well-order, then $y_{\alpha }$ to the least eligible ${\tau }_{\alpha }$-play outside the used set and $\{x_{\alpha }\}$. Define the rule on any malformed history or empty eligible set to be the constant-zero pair. It is a single-valued total set rule; F5 gives its recursion through $\kappa$. Step 2.1 inductively ensures the default is never used on the actual history, and all selected points are pairwise distinct.

Put $A=\{y_{\alpha }:\alpha <\kappa \}$. For each I strategy ${\sigma }_{\alpha }$, its compatible play $x_{\alpha }$ is outside $A$, including outside all later selected points by step 3.1. Thus it loses on that play. For each II strategy ${\tau }_{\alpha }$, its compatible $y_{\alpha }$ is in $A$, so it loses on that play. Neither player has a winning strategy. AD asserts determinacy for this very natural-number payoff, so it cannot hold together with AC. No cofinality or regularity assumption on $\kappa$ occurred. QED.