The following question is about the possibility of having a world of sets obeying new foundations "NF" with their well founded sets obeying rules of ZF. It uses the revised version of Quines $``ML"$ (Mathematical Logic) system, in order to define well foundedness in a faithful manner, and then adds axioms of size and infinity over the well founded sector.
Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$
Classes: if $\phi$ is a formula in which $x$ doesn't occur free, then $(\exists x \forall y (y \in x \leftrightarrow y \in V \land \phi))$
Define: $x=\{y\in V| \phi\} \iff \forall y (y \in x \leftrightarrow y \in V \land \phi)$
Stratification: if $\phi(y,x_1,..,x_n)$ is a stratified formula in which $x$ doesn't occur free, and in which all quantifiers are bounded by $V$, and all free variables of it are among $y,x_1,..,x_n$ then:$$\forall x_1 \in V,...,\forall x_n \in V (\{y\in V| \phi\} \in V)$$
Size: $x,y\text{ are well founded} \land |x|=|y| \land x \in V \to y \in V$
Where: $\text{well founded} (x) \iff \\\not \exists d (x \cap d \neq \emptyset \land \forall m \in d \exists n \in d (n \in m))$
Infinity: $\omega \in V$
Where $\omega$ is the set of all finite Von Neumann ordinals.
Question: Is this theory consistent relative to consistency of $NF$ and $ZF$?