Working in bi-sorted first order logic with equality and membership. First sort variables written in lower case range over sets. Second sort variables written in upper case range over classes. Lets have all bi-sorted equality theory axioms, and axioms stating that every set is a class, and every element of a class is a set, and a comprehension axiom scheme stipulating the existence a class $\{x\mid \phi\}$ for every formula (parameters allowed) with all of its variables written in lower case.
We say a unary predicate $\Psi$ is an encompassing-subspecies of a unary predicate $\Phi$, denoted $\Psi \ll \Phi$, if and only if: $$\forall X: \Psi(X) \to \Phi(X) \\\forall X: \Phi (X) \to \exists Y: \Psi (Y) \land X \subseteq Y $$
Define: $\operatorname {Trs}(X) \iff \forall y \in X: y \subseteq X$
- SETS: for each formula $\phi$ that doesn't use "$l$" nor "$y$", and for each definable unary predicate $\Psi$ ; we have: $$ \Psi \ll \operatorname {Trs} \land \ \exists x: \Psi(x) \\\to \\ \forall \vec{p} \, \bigl [ \forall a \exists c \forall b \, (\phi(a,b) \to b=c)\\ \to \\ \forall k \, \exists l \ni k : \Psi(l) \land \\ \forall x \in l \exists!y \in l: y=\{b| \exists a \in x: \phi(a,b) \} \bigr] $$
When $\Psi$ is $\operatorname { Trs}$ we get all axioms of $\sf ZF$-$\sf Reg.$-$\sf Powersets$. When $\Psi$ is $\operatorname {supertransitive}$ we get $\sf ZF$-$\sf Reg.$
My suspicion is that set-inaccessible (unreachable by powering and unions from below via set-injections) supertransitivity is an encompassing-subspecies of transitivity, and since there exists such a set, then we'd have set-inaccessible sets, which is something $\sf ZFC$ cannot prove.
Can this theory prove the consistency of $\sf ZFC$?
