In $\mathsf{ZFC}$ if any two proper class models of the theory of an infinite set are isomorphic, then global choice holds. This is because $V$ and $\mathrm{Ord}$ are both models of this theory and an isomorphism between them gives a global well-ordering of $V$.
Edit: As I mentioned in the comments, Elliot had an idea for resolving a more general version of the saturation question. Specifically we have the following.
Proposition 1. There are formula $\varphi_0(x,m,\ell)$ and $\psi(x,m,F)$ in the language of set theory (with $F$ a second-order class function variable but such that $\psi$ has only first-order quantifiers) such that for any language $L$ and any infinite $L$-structure $M$,
- $\varphi_0(x,M,L)$ defines a saturated proper class elementary extension $\mathbb{M}_0$ of $M$ (with a definable satisfaction relation defined by a formula that I'm not going to give an explicit name) and
- if $F$ is any definable injection from $\mathrm{Ord}$ to $\mathbb{M}_0$, then $\psi(x,M,L,F)$ defines a global choice function.
Proposition 2. There is a formula $\varphi_1(x,m,\ell,u)$ in the language of set theory such that for any language $L$, any infinite $L$-structure $M$, and any non-principal ultrafilter $U$ on $M$, $\varphi_1(x,M,L,U)$ defines a saturated proper class elementary extension $\mathbb{M}_1$ of $M$ (again with a definable satisfaction relation) such that there is a definable injection from $\mathrm{Ord}$ into $\mathbb{M}_1$.
Combining these we obviously get that any definable injection from $\mathbb{M}_1$ into $\mathbb{M}_0$ gives global choice. I haven't tracked the complexity of the formula $\psi$, but Elliot's comment suggests that it should be doable with only two quantifiers.
Both of these constructions are going to be modifications of Kanovei and Shelah's construction of proper class monster models in A Definable Nonstandard Model of the Reals. Elliot's original idea was to use the basic Kanovei-Shelah construction for $\mathbb{M}_0$. I think that probably does work, but I found it easier to verify that the modified construction I'm going to sketch out works.
Recall that an $L$-structure $M$ has Skolem functions if for every for every $L$-formula $\varphi(\bar{x},y)$, there is a function symbol $f(\bar{x})$ such that $M \models \forall\bar{x}(\exists y \varphi (\bar{x},y) \to \varphi(\bar{x},f(\bar{x}))$. Recall that $M$ has quantifier elimination if for every $L$-formula $\varphi(\bar{x})$, there is an atomic predicate $P(\bar{x})$ such that $M \models \forall\bar{x}(\varphi(\bar{x}) \leftrightarrow P(\bar{x})$.
Lemma 1. There is a definable map that takes a language $L$ and an $L$-structure $M$ and produces an expanded language $L' \supseteq L$ and an expansion $M'$ such that $M'$ has Skolem functions and quantifier elimination.
Proof. It is sufficient to take the complete expansion of $M$ (i.e., add all subsets of $M^n$ as atomic predicates and all functions $f:M^n \to M$ as function symbols). $\square$
Using Lemma 1, we can assume without loss of generality that the structure $M$ we start from has Skolem functions and quantifier elimination. (In particular, this makes it easy to verify that the resulting class structure has a definable satisfaction relation.)
Iterated ultrapowers
Kanovei and Shelah use the idea of a iterated ultrapower (iterated along an arbitrary linear order). Given a structure $M$, a linear order $(I,<)$, and a family $(U_i)_{i \in I}$ of ultrafilters, the iterated ultrapower of $M$ with regards to the family $(U_i)_{i \in I}$ is the directed colimit of the diagram of ultrapowers of $M$ by finite products of the $U_i$'s. In other words, for any finite set $\{i_1 < i_2 < \dots < i_n\}= I_0 \subseteq I$, we have the ultrapower $M_{I_0} := M^{U_{i_1} \otimes U_{i_2}\otimes \dots \otimes U_{i_n}}$. Given any two finite sets $I_0,I_1 \subseteq I$ with $I_0 \subseteq I_1$, there's a canonical inclusion map from $M_{I_0}$ into $M_{I_1}$ and these inclusion maps give a functor from the poset of finite subsets of $I$ to the category of $L$-structures with embeddings. The iterated ultrapower is the colimit of this diagram (which will be an elementary extension of $M$ by a standard model-theoretic argument). We'll write $M^{\bigotimes_{i \in I} U_I}$ for the iterated ultrapower (even though this is a mild abuse of notation).
Since we want to do everything definably (and our goal is also to ultimately hide some extra data in this construction), we should spell out how we're specifically coding this. We'll need the following fact which is not too hard to prove but becomes a little bit of a notational hassle to spell out.
Lemma 2. For every $a \in M^{\bigotimes_{i \in I} U_i}$, there is a unique smallest finite set $I_0 \subseteq I$ such that $a \in f(M_{I_0})$ (where $f : M_{I_0} \to M^{\bigotimes_{i \in I} U_i}$ is the canonical inclusion map). $\square$
We'll call this $I_0$ the support of $a$.
With this fact in hand, we'll officially define the literal set-codings of elements of $M^{\bigotimes_{i \in I} U_i}$ in a cut-and-paste manner:
- The canonical inclusion map from $M$ to $M^{\bigotimes_{i \in I} U_i}$ is the identity map (so that the underlying set of $M^{\bigotimes_{i \in I} U_i}$ is a literal superset of the underlying set of $M$).
- Elements of $M^{\bigotimes_{i \in I} U_i}$ that are not in $M$ are represented as tuples $(a,M,M_{I_0},i_1,i_2,\dots,i_n)$ where $I_0 = \{i_1 < \dots < i_n\}$, $a \in M_{I_0}$, and the support of $a$ is $I_0$ (and $M_{I_0}$ is defined in the standard way in terms of equivalence classes in the product).
(The extra $M$ is in that tuple just out of paranoia, but it's probably unnecessary.)
Realizing one coheir
Given an $L$-structure $M$ with Skolem functions and an ultrafilter $U$ on $M$, there's a canonical elementary extension $M[U]$ of $M$ that realizes the type over $M$ that is specified by the ultrafilter $U$. (In model-theoretic terminology, this type is called the coheir corresponding to $U$.) There's a lot of ways of building this but the easiest is to just take the ultrapower $M^U$ and then consider the Skolem hull of $M$ together with the $U$-equivalence class $[\mathrm{id}]_U$ of the identity function on $M$. (Historical note: This is essentially the technique of Skolem's original construction of a non-standard model of arithmetic.) Just like before I want to define this to be a literal superset of $M$, but also to make my life a little bit easier later on I want to include an extra bit of data. Given an ordinal $\alpha$ and a non-principal ultrafilter $U$ on $M$, we'll let $M[U,\alpha]$ be the elementary extension of $M$ whose elements are
- the elements of $M$,
- $([f]_U,M)$ for elements $[f]_U$ of $M^U$ that are in the Skolem hull of $M$ and $[\mathrm{id}]_U$ but are not equal to $[\mathrm{id}]_U$ or to $[c]_U$ for any constant function $c : M \to M$, and
- $([\mathrm{id}]_U,M,\alpha)$ (which is playing the role of $[\mathrm{id}]_U$).
This is of course leading up to the definable injection of $\mathrm{Ord}$ into $\mathbb{M}_1$.
Again the $M$ is there to avoid collision. Also note that none of these new elements can ever be equal to the new elements in the iterated ultrapower construction as literal sets (since they're tuples of different length).
Construction of $\mathbb{M}_0$ and proof of Proposition 1
The Kanovei-Shelah construction relies on the following fact.
Lemma 3. There is a definable map that takes a cardinal $\kappa$ and produces a linear order $(I_\kappa, <)$ and a family $(U_{\kappa,i})_{i \in I_\kappa}$ of non-principal ultrafilters on $\kappa$ such that for every non-principal ultrafilter $F$ on $\kappa$, there is an $i \in I_\kappa$ such that $F = U_{\kappa,i}$.
Proof. Let $\lambda = |2^\kappa|$. There's a canonical lexicographic ordering on the power set $2^{\kappa \cdot \lambda}$ of $\kappa\cdot \lambda$ (where $\kappa \cdot \lambda$ is the ordinal product of $\kappa$ and $\lambda$). We can take $I$ to be the set of elements of $2^{\kappa\cdot \lambda}$ that code $\lambda$-enumerations of ultrafilters on $\kappa$. $\square$
Now we need to modify this linear order a little bit in order to sneak in more data. Similarly to the previous proof, for any cardinal $\kappa$, let $(J_\kappa,<)$ be the set of elements of $2^{\kappa \cdot \lambda}$ that are $\lambda$-enumerations of the full power set of $\kappa$ with the same canonical lexicographic order. Let $K_\kappa$ be the product order $I_\kappa \times J_\kappa$ (with the lex order on pairs). Finally, let $(U^\ast_{\kappa,(i,j)})_{(i,j) \in K_\kappa}$ be the family of ultrafilters defined by $U^\ast_{\kappa,(i,j)} = U_{\kappa,i}$.
Now finally we can define $\mathbb{M}_0$ by transfinite recursion:
- Let $\mathbb{M}_0(0) = M$.
- Given $\mathbb{M}_0(\alpha)$, let $\mathbb{M}_0(\alpha+1) = \mathbb{M}_0(\alpha)^{\bigotimes_{k \in K_{\aleph_\alpha}} U^\ast_{\aleph_\alpha,k}}$.
- For limit $\lambda$, let $\mathbb{M}_0(\lambda) = \bigcup_{\alpha < \lambda} \mathbb{M}_0(\alpha)$.
Finally $\mathbb{M}_0$ is $\bigcup_{\alpha \in \mathbb{Ord}}\mathbb{M}_0(\alpha)$. It's relatively straightforward to now show that $\mathbb{M}_0$ is a saturated elementary extension of $M$ (and that its satisfaction class is definable by our use of Lemma 1).
Proposition 1. There is a uniform way to define a global choice function from any definable injection $F : \mathrm{Ord} \to \mathbb{M}_0$.
Proof. For any $\kappa$, we can definably find a well-ordering of $2^\kappa$. Find the smallest $\alpha$ such that $F(\alpha)$ is of the form $(\_,\_,\_,k_1,k_2,\dots,k_n)$ where $k_1 = (i,j)$ and $j$ codes a well-ordering of $2^\mu$ for some $\mu \geq \kappa$. (This must exist by the proper class pigeonhole principle.) We can then restrict this to a well-ordering of $2^\kappa$. By a standard argument we can now use these to inductively define well-orderings of $V_\alpha$ for every $\alpha$. $\square$
Construction of $\mathbb{M}_1$ and proof of Proposition 2
Given all the machinery we've built up to this point, this is now fairly straightforward. Fix an ultrafilter $F$ on $M$. Define $\mathbb{M}_1$ by transfinite recursion:
- $\mathbb{M}_1(0) = M$.
- $\mathbb{M}_1(\alpha +1) = (\mathbb{M}_1(\alpha)[F_\alpha,\alpha])^{\bigotimes_{i \in I_{\aleph_\alpha}}U_{\aleph_\alpha,i}}$, where $F_\alpha$ is the canonical extension of $F$ to an ultrafilter on $\mathbb{M}_1(\alpha) \supseteq M$.
- $\mathbb{M}_1(\lambda) = \bigcup_{\alpha < \lambda} \mathbb{M}_1(\alpha)$ for limit $\lambda$.
Then $\mathbb{M}_1 = \bigcup_{\alpha \in \mathrm{Ord}}\mathbb{M}_1(\alpha)$. Just like before it is straightforward to show that this is a saturated proper class elementary extension of $M$ with a definable satisfaction relation.
Proposition 2. There is a definable injection from $\mathrm{Ord}$ into $\mathbb{M}_1$.
Proof. By construction there is exactly one element of $\mathbb{M}_1$ of the form $(\_,\_,\alpha)$ for each sufficiently large ordinal $\alpha$ (or every $\alpha$ if we arrange so that no element of $M$ is of this form). This gives the required injection. $\square$
