I need a global choice function defined by a formula in (a fragment of) ZF. There is no harm in assuming V=L for my purposes. But I wonder if there are any familiar alternative ways to get this?

The comments make see I also want a weakened part of GCH. Namely the power set of $\aleph_n,\ n\in\mathbb{N}$ should be $\aleph_m$ for some $m\in\mathbb{N}$. I see that HOD is known compatible with some extreme failure of CH, but I have not found what. Is it compatible with failure of this weakened part of GCH?