 Rank-shifting NFU model with explicit set predicate

Let $M$ be a membership structure satisfying extensionality and every pure-membership separation instance, with an external automorphism $j$ and domains $D_i=j^i(D_0)$ represented by objects of $M$. Suppose every $M$-subset of $D_i$ is an element of $D_{i+1}$. Interpret NFU on the objects of $D_0$ using the displayed set predicate and membership, with all subset statements evaluated in $M$. Atoms have no members, and extensionality applied to $j(y),j(z)\subseteq D_0$ gives extensionality for sets. A stratified formula becomes an ordinary pure-membership formula by sending each variable of type $i$ to $j^i(x)$ and restricting its quantifier to $D_i$. A set predicate on sort $i$ means containment in $D_{i-1}$; adjacent-sort membership is guarded by containment in the lower domain. Separation yields the extension $X\subseteq D_i$, the closure hypothesis places it in $D_{i+1}$, and $j^{-(i+1)}(X)\in D_0$ is the required untyped set. This proves every comprehension instance. The guard is essential: an object not contained in a lower domain can still have some ordinary members there, which must not become members of a typed atom. Internal ranks $V_{j^i(\alpha )}$ with $j(\alpha )>\alpha$ give one instance of these hypotheses; shifted rank objects in an elementary model of an expanded $V_{\omega +\omega }$ give a consistency proof without assuming Con(ZFC).