I believe you can find a proof in Foreman and Magidor, "Large cardinals and definable counterexamples to CH".

@MohammadGolshani Thanks for the reference. It looks like a large antichain is explicitly constructed; no hint on the surface as to whether it collapses $\aleph_2$.

It's amazing that this abstract logical judo would have any bearing on Twin Primes.

I admit though that my answer is probably off because it doesn't seem that the more recent results add weight to the argument against the HOD conjecture. (At least as I've framed it; maybe Bagaria has more to say.)

@GabeGoldberg But these choiceless cardinals have been studied for a long time, including by Woodin himself. Was there a special reason he thought he was on the way to refuting them? By analogy one might come up with some combinatorial statement about $H_{\omega_4}$ that one conjectures should be a ZFC theorem, but if supercompacts show that the negation is consistent, then in practice that settles the question. It would be weird to hold on to the original intuition and insist that this is evidence for the inconsistency of supercompacts.

What about stating Zorn’s Lemma only for the case of partial orders of subsets of a given set ordered by inclusion?

@DavidRoberts I always interpreted these quotes in the blog as describing what subsets of the ZF axioms are needed for BD, in particular that the subtheory Z is not enough.