Power ${\mathrm{\Sigma }}_1$ in Card with two Woodin cardinals

Väänänen and Welch asked in the paper “When cardinals determine the power set: inner models and Härtig quantifier logic” which large cardinals are consistent with the power set operation $x\mapsto P(x)$ being ${\mathrm{\Sigma }}_1$-definable in the predicate Card of all cardinals. We show that, relative to large cardinals, this property is consistent together with the existence of two Woodin cardinals.