In this posting, I've define stratified power sets $\mathcal P^\equiv$ operator.

Now we define $V^\equiv_\alpha$ as the iterative stratified power sets of $V_\omega$ as:

$$V^\equiv_0 = V_\omega \\ V^\equiv_{\alpha+1} = \mathcal P^\equiv(V^\equiv_\alpha) \\ V^\equiv_\alpha = \bigcup^{\beta < \alpha} V^\equiv_\beta, \text { for limit } \alpha $$

Its clear that those powers are defined in $\sf ZFC^- + R \text{ well orders } V - Power + \text { every set is countable } $ which is known to be equivalent to second order arithmetic "$\sf 2OA$ "

Now since this theory has an infinite model, then there is a model of it that admits an external automorphism $j$ that shift ranks inwardly, i.e. there is an ordinal $\alpha$ such that $j(\alpha) < \alpha$ and such that there is a stage $V_{\alpha + 1}$ that is moved inwardly, i.e. $V_{j(\alpha)+1}$ is a proper subset of $V_\alpha$. So the above theory + existence of that external (not appear in instances of separation and replacement) automorphism is equi-consistent with $\sf 2OA$.

My question is equiconsistent with $\sf 2OA$ that there exists an automorphism $f$ that moves an infinite limit ordinal $\alpha$ such that $V^\equiv_{j(\alpha)+1} \subsetneq V^\equiv_\alpha$

If not, then is it provable for the above assertion to be consistent with the above theory in some stronger theory? And what would be that proof or that level of strength?

The rationale behind question 1 is that it might be the case that only ranks indexing finite $V_\alpha$ stages can be moved dowardly and so the infinite stratified ranks might be fixed by $j$? However, I'm not sure if this is a possiblity, hence my question.

The rationale behind question 2 is that perhaps working in a stronger theory like Zermelo for example can prove existence of a model of it with an external automorphism that would move a stratified power stages with an infinite rank inwardly along the $V_\alpha$ stages that are moved by it, since those stratified powers would be subsets of those stages.