The folloing is an Edit of the previous question.

By stratified acyclic ZF, it is meant acylic ZF but with restricting Separation and Replacement to stratified instances of them.

Is Stratified acyclic ZF consistent with having an internal non-trivial automorphism $j$ from $V$ to $V$?

That is we add a new primitive one place function symbol $j$ to the language of ZF, and add the axioms of $j$ being an automorphism over the whole universe of discourse, that is:

Bijectivity: $\forall x \exists y : j(x)=y \\\forall y \exists x: j(x)=y$

Isomorphism: $\forall x \forall y :x \in y \iff j(x) \in j(y)$

Collapse: $\exists \alpha: V_\alpha \subsetneq V_{j(\alpha)}$

Where $``j"$ is allowed to appear in instances of the stratified separation and replacement.

If this is allowed what would be the consistency strength of such addition?

The folloing is an Edit of the previous question.

By stratified acyclic ZF, it is meant acylic ZF but with restricting Separation and Replacement to stratified instances of them and forbid the use of symbol $\mathcal R$ them.

Is Stratified acyclic ZF consistent with having an internal non-trivial automorphism $j$ from $V$ to $V$?

That is we add a new primitive one place function symbol $j$ to the language of ZF, and add the axioms of $j$ being an automorphism over the whole universe of discourse, that is:

Bijectivity: $\forall x \exists y : j(x)=y \\\forall y \exists x: j(x)=y$

Isomorphism: $\forall x \forall y :x \in y \iff j(x) \in j(y)$

Collapse: $\exists \alpha: V_\alpha \subsetneq V_{j(\alpha)}$

Where $``j"$ is allowed to appear in instances of the stratified separation and replacement.

If this is allowed what would be the consistency strength of such addition?

By stratified acyclic ZF, it is meant acylic ZF but with restricting Separation and Replacement to stratified instances of them.

Is Stratified acyclic ZF consistent with having an internal non-trivial automorphism $j$ from $V$ to $V$?

That is we add a new primitive one place function symbol $j$ to the language of ZF, and add the axioms of $j$ being an automorphism over the whole universe of discourse, that is:

Bijectivity: $\forall x \exists y : j(x)=y \\\forall y \exists x: j(x)=y$

Isomorphism: $\forall x \forall y :x \in y \iff j(x) \in j(y)$

Collapse: $\exists \alpha: V_\alpha \subsetneq V_{j(\alpha)}$

Where $``j"$ is allowed to appear in instances of the stratified separation and replacement.

If this is allowed what would be the consistency strength of such addition?

The folloing is an Edit of the previous question.

By stratified acyclic ZF, it is meant acylic ZF but with restricting Separation and Replacement to stratified instances of them.

Is Stratified acyclic ZF consistent with having an internal non-trivial automorphism $j$ from $V$ to $V$?

That is we add a new primitive one place function symbol $j$ to the language of ZF, and add the axioms of $j$ being an automorphism over the whole universe of discourse, that is:

Bijectivity: $\forall x \exists y : j(x)=y \\\forall y \exists x: j(x)=y$

Isomorphism: $\forall x \forall y :x \in y \iff j(x) \in j(y)$

Collapse: $\exists \alpha: V_\alpha \subsetneq V_{j(\alpha)}$

Where $``j"$ is allowed to appear in instances of the stratified separation and replacement.

If this is allowed what would be the consistency strength of such addition?

By stratified ZF -Reg., it is meant the theory ZF - Reg. with restricting Separation and Replacement to stratified instances of them.

Is Stratified ZF consistent with having an internal non-trivial automorphism $j$ from $V$ to $V$?

That is we add a new primitive one place function symbol $j$ to the language of ZF, and add the axioms of $j$ being an automorphism over the whole universe of discourse, that is:

Bijectivity: $\forall x \exists y : j(x)=y \\\forall y \exists x: j(x)=y$

Isomorphism: if $\phi(x_1,..,x_n)$ is a formula with $x_1,..,x_n$ being all of its free variables, then $$\forall x_1,..,\forall x_n \ [ \phi(x_1,..,x_n) \iff \phi(j(x_1),..,j(x_n))]$$

Critical point: $\exists x: x < j(x)$

Where: $x < j(x) \iff \mathcal Ord(x) \land x \in j(x)$

Where: $\mathcal Ord(x) \iff \forall y \in x (y \not \in y) \land trs(x) \land \forall y \in x(trs(y))$

Where: $trs(x)$ stands for $x$ is transitive, i.e. every element of $x$ is a subset of $x$.

Where $``j"$ is allowed to appear in instances of the stratified separation and replacement.

If this is allowed what would be the consistency strength of such addition?

By stratified acyclic ZF, it is meant acylic ZF but with restricting Separation and Replacement to stratified instances of them.

Is Stratified acyclic ZF consistent with having an internal non-trivial automorphism $j$ from $V$ to $V$?

That is we add a new primitive one place function symbol $j$ to the language of ZF, and add the axioms of $j$ being an automorphism over the whole universe of discourse, that is:

Bijectivity: $\forall x \exists y : j(x)=y \\\forall y \exists x: j(x)=y$

Isomorphism: $\forall x \forall y :x \in y \iff j(x) \in j(y)$

Collapse: $\exists \alpha: V_\alpha \subsetneq V_{j(\alpha)}$

Where $``j"$ is allowed to appear in instances of the stratified separation and replacement.

If this is allowed what would be the consistency strength of such addition?