I'm in the proof of showing, that the consistency of 2-huge cardinals implies the consistency of hyper-huge cardinals and it needs this equivalence:
Let $\kappa,\kappa',\lambda,\lambda'$ be cardinals. I want to show the equivalence of the existence of a normal ultrafilter U on $\mathcal{P(\lambda')}$ with $\{ x\subseteq\lambda'\vert x \cap\kappa\in\kappa,\text{otp}(x\cap\kappa')=\kappa, \text{otp}(x)=\lambda\}\in U$ and the existence of an elementary embedding $j\colon V \to M$ for some M with:
(1) $crit(j)=\kappa$
(2) $\lambda<j(\kappa)=\kappa'$
(3) $\lambda'=j(\lambda)$
(4) $^{\lambda'}M \subseteq M$
So far i have shown the existence of the ultrafilter if there is such an embedding. But for the other direction i wanted to ask, if it's the right way to just build the ultrapower like in the normal equivalence with measurable cardinals but with $\mathcal{P(\lambda')}$ as an index? If not, could maybe someone give me a hint on what to do?
Edit: I think now i can show everything but $\lambda < j(\kappa)$. I don't see why this should be true. It seems to me, that the ultrafilter gives no correspondence of $\kappa$ and $\lambda$. Does anybody have a hint for me, why this should be true?
Edit 2: I could change the set, which need to be in the ultrafilter to $\{ x\subseteq\lambda'\vert x \cap\kappa\in\kappa,\text{otp}(x\cap\kappa')=\kappa, \text{otp}(x)=\lambda, \text{otp}(x \cap \lambda)<\kappa\}$ and because the new condition is equivalent to $\lambda <j(\kappa)$ it would be in $U$ if you assume such an embedding. But is it necessary to add this?