I need to know if the following system is consistent, because I want to use it in presenting automorphisms over stratified versions of it.

The system I'd label as "*Acyclic ZF*", which is $\small \sf ZF-Reg.+ acyclic \ AFA + Rank$, is obtained by adding a two place predicate symbol $\mathcal R$ symbolizing *is the rank of* to the language of $\small \sf ZF$, then replace Regularity by the following two acyclic AFA axioms:

**Acyclicity:** $\forall x_1,..,x_n: \neg (x_1 \in x_2 \in x_3 \in ... \in x_n \land x_1=x_n)$

**Acyclic construction:** For every *acyclic* accessible pointed graph there exists a set whose membership graph is isomorphic to it, where the latter means the membership map on the transitive closure of that set.

Now we define the unary predicate *ordinal*, symbolized by $\mathcal Ord$, as *transitive set of transitive sets*. To be emphasized here is that an ordinal can be a von Neumann or may not be so! If the ordinal is well founded on $\in$, then it is a von Neumann ordinal, if not then its to be called as a non-standard ordinal, or even more outrageously an *ill-founded ordinal*. We make axioms to the effect that the ranking relation $\mathcal R$ constitute a partial function from ordinals to sets such that the indexed sets would correspond to iterative powers similar to the buildup of the cumulative hierarchy. Formally this is:

$\forall a,b,c,d: \mathcal R(a,b) \land \mathcal R(c,d) \longrightarrow [a=c \Leftrightarrow b=d]$

$\forall x: \exists y (\mathcal R (x,y)) \iff \mathcal Ord(x)$

$\forall \alpha \forall x \forall y: \mathcal R(\alpha, x) \land \mathcal R (\alpha \cup \{\alpha \}, y) \longrightarrow y=\mathcal P(x)$

$\forall \alpha \forall x [(\not \exists \beta: \alpha=\beta \cup \{\beta\}) \land \mathcal R(\alpha,x) \longrightarrow \\ x= \bigcup \{y: \exists \beta \in \alpha ( \mathcal R(\beta,y)) \}]$

$\forall \alpha \forall x : \mathcal R(\alpha,x) \to \alpha \subseteq x \land \alpha \not \in x$

$\forall \alpha \forall x: \mathcal R (\alpha, x) \to \forall y \in x (y \subseteq x)$

The last axiom is to restrict sets to those itrative stages, I'll consider it as a parallel to foundation, that is:

**Para-foundation:** $\forall x \exists \alpha \exists v : \mathcal R(\alpha, v) \land x \in v$

Now, is Acyclic ZF consistent?