**Edit:** Here's my preprint filling in the details of the construction in this answer: https://arxiv.org/pdf/2312.11902.pdf

Global Choice is not conservative over ZC. We'll build a model of ZC which satisfies a sentence disprovable by Global Choice. Warning: it is hideous, and I've been struggling to come up with a clean way to present it.

We work in ZF + GCH below $\aleph_{\omega}$ + existence of countable sets $(X_n)_{n<\omega}$ such that there is a surjection $f: \mathcal{P}(\bigcup_{n<\omega} X_n) \rightarrow \omega_2.$ This holds in a symmetric extension of $L$, see Asaf Karagila's *Iterated failures of choice*, section 4.

The model we construct will satisfy ZC + GCH and that every infinite set has cardinality some $\aleph_n,$ yet will code $(X_n)_{n<\omega}$ and $f$ by definable classes. Note that we are identifying $\aleph_n$ with the canonical prewellordering of $\mathcal{P}^n(\omega)$ of length $\omega_n$ since the von Neumann construction of the $\aleph$'s doesn't work in ZC.

Let $X = \bigcup_{n<\omega} X_n.$ There will be Quine atoms $a_x$ for each $x \in X$ and $a_Y$ for each $Y \subset X.$

Let $B = \{V_{\omega}\} \cup \{\{a_x: x \in X_n\}: n<\omega\}\cup \{\{a_Y\}: Y \subset X\}.$

Consider this model:

$$M_1=\bigcup_{n<\omega}\bigcup_{S \in [B]^{<\omega}} \mathcal{P}^n(\bigcup S).$$

Then $M_1 \models ZC + GCH + \forall S \exists n (|S| \le \aleph_n).$

Let $P = \{(n, a_x): x \in X_n\} \cup \{(a_x,a_Y): x \in Y \subset X\} \cup \{(a_Y, f(Y)): Y \subset X\}.$ We will build an extension of $M_1$ in which $P$ is a definable predicate. For each $p \in P,$ let $b_p = \{p, b_p\}.$

Let $C = B \cup \{\{b_p\}: p \in P\}.$

Let $M = \bigcup_{n<\omega}\bigcup_{S \in [C]^{<\omega}} \mathcal{P}^n(\bigcup S).$

Then $M \models ZC + \varphi,$ where $\varphi$ is the conjunction CH $\wedge$ $``$the class $\{p: \exists b (b=\{b, p\})\}$ codes a countable sequence of countable sets of atoms $X_n,$ a class of atoms which each relate to a different subclass of $\bigcup_{n<\omega} X_n,$ and a surjection from the latter class onto $\aleph_2."$

Finally, we see that Global Choice proves $\neg \varphi,$ since from a global choice function, we can choose enumerations of each $X_n,$ enumerate $\bigcup_{n<\omega} X_n,$ and thus define a surjection from $\mathcal{P}(\omega)$ onto $\omega_2,$ violating CH.

Also note that we can adjust the construction of $M$ so that it satisfies Foundation by several applications of the trick used here: Is $\in$-induction provable in first order Zermelo set theory?

1more comment