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 )$