Is $\alpha < \beta \to 2^\alpha < 2^\beta$ provable in ZF+V=HOD? Is the following a theorem of ZF + V=HOD?
$\kappa < \lambda \to 2^\kappa < 2^\lambda$
Where $<$ is cardinal strictly smaller than.
I know that this is not a theorem of ZFC. Of course, it is a theorem of ZFC+ V=L. However ZF+V=HOD doesn't prove CH. So can it prove the above statement?
 A: No, of course not.
Lemma. Every set of ordinals appears in the $\sf HOD$ of a generic extension which agrees on the power set of whatever fixed $\lambda$.
Sketch of Proof. Let $A\subseteq\alpha$ be a set of ordinals. Pick some large enough $\kappa$, and force $\sf GCH$ to hold between $\kappa$ and $\kappa^{+\alpha}$ by means of forcing and without adding new subsets to $\lambda$. Next, force that $2^{\kappa^{+\beta+1}}=\kappa^{+\beta+3}$ if and only if $\beta\in A$. We can do that without adding subsets to $\lambda$ as well.
Now $A$ is definable from the parameters $\kappa$ and $\alpha$, since it is exactly the failure of $\sf GCH$ in the first $\alpha$th successors of $\kappa$.

Now, start with a model of $\sf GCH$, add $\aleph_2$ Cohen reals, so that $2^{\aleph_0}=2^{\aleph_1}=\aleph_2$. Next, consider the Cohen reals as a subset of $\omega_2\times\omega$, and code this into a set of ordinals $A$ (either via the Gödel pairing function, or simply in the naive way of looking at this as a subset of the ordinal $\omega_2\cdot\omega$).
Then code $A$ into $\sf HOD$ of some generic extension without adding any new subsets to $\omega_2$.
