Let $R$ be a relation definable in the language of set theory. We call $R$ as inherently proper class relation over domain $D$ if it and its complementary output over domain $D$ are proper classes, i.e. for each $x$ the class of all $y \in D$ such that $y R x$ is a proper class, and the class of all $y \in D$ such that $ y \not R x $ is also a proper class.
We recursively define $\in^n$ as:
$y \in^0 x \leftrightarrow y=x$
$y \in^{n+1} x \leftrightarrow \exists z (z \in^n x \land y \in z)$
Define $R^n$ recursively as:
$y R^0 x \leftrightarrow y=y$
$y R^{n+1} x \leftrightarrow y R^n x \land \forall z \in^n y (z R x)$
We say a relation is hereditarily shrinking if and only if for each $n>0$:$\ R^n$ is inherently proper class relation over its prior domain. That is, for each $x$ the class of all $y$ such that $y R^{n-1} x \land y R^n x$ is a proper class, and the class of all $y$ such that $y R^{n-1} x \land \neg y R^n x$ is a proper class too.
Is the following provable in $ZFC$?
$R \text { is hereditarily shrinking } \to \forall x \exists s (s=\{y|\forall n \in \omega (y R^n x)\}) $
The above schema is inconsistent with ZF.
Take the $x R y$ to be $x=x \land (y \text{ is singleton} \lor y\text{ is a set of singletons})$
Clearly $R$ is hereditarily shrinking relation, yet the class of all sets $y$ hereditarily satisfying $R$ (for whatever $x$) is indeed a proper class.