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?