Working in bi-sorted FOL, where lower cases stand for sets and upper cases for classes; add all axioms of ZF written completely in lower case, and add an axiom of Extensionality over all classes, and the following axioms:

$\forall x \ \exists Y: Y=x$

$\forall X \ \forall Y: X \in Y \to \exists z: z=X$

$\forall \vec{Z} \ \exists X \ \forall y \ (y \in X \iff \phi(y, \vec{Z}))$; if $\phi(y, \vec{Z})$ is a formula not using $X$.

Is there a clear inconsistency with the following principle?

Define recursively: $J_0``x = J(x) \\ J_{n+1} `` x= \{J_n`` y \mid y \in x \}$

Internalization schema:$n=1,2,... \\ \forall \text { infinite } x,y \ \exists J \ ( J: x \rightarrowtail y \land \forall s: J_n ``s \in V )$