>Is it possible to iterate elementary embeddability and reflect on those stages that are elementary embeddable to themselves?

The following is a formal capture of that idea:

 To the language of $\sf ZF$ (i.e., mono-sorted $\sf FOL(=,\in)$) add primitive partial unary functions $W$ and $j$. 

To the axioms of $\sf ZF$, add the following axioms:

**Restriction:** $\forall \alpha: W_\alpha \lor j_\alpha \to \operatorname {ordinal}(\alpha)$

**Injectivity:** $W_\alpha \land W_\beta \land \alpha \neq \beta \to W_\alpha \neq W_\beta$



**Cumulation:** $\forall \alpha \exists \lambda: W_\alpha=V_\lambda$



**Elementarity:** $\forall \alpha \, (j_\alpha: W_\alpha \to W_\alpha  \land \\ \forall \vec{x} \in W_\alpha [ \phi(\vec x) \leftrightarrow \phi(j_\alpha[\vec x ])] \land \\ \exists x: j_\alpha (x) \neq x)$

**Reflection:** $\forall \vec{x} (\phi \to \exists \alpha: \phi^{W_\alpha}); \text { if } \alpha \text { doesn't occur in } \phi$


Where $V_\lambda$ stands for the $\lambda^{th}$ stage of the cumulative hierarchy, defined in the customary manner. $\phi^X$ stands for relativising all quantifiers in $\phi$ to $``\in X\!"$.

> Is the above theory consistent relative to some large cardinal property? If so, Which one?