This is a first order set theory, with the purpose of interpreting $\sf NF$ set theory:

Extensionality: $\forall X \forall Y: \forall z (z \in X \leftrightarrow z \in Y) \implies X=Y$

Empty: $\exists X: \forall y \ (y \not \in X)$

Pairing: $\forall A \forall B \exists X: X=\{A,B\}$

Relative Complements: $\forall A \forall B: A \subset B \to \exists C: C=\{x \in B| \ x \not \in A\}$

Set union: $\forall A \exists X: X=\bigcup A$

Power: $\forall A \exists X: X=\mathcal P(A)$

Composition: $\forall Q \forall S \exists R: R=\{\langle q,s \rangle| \ \exists r: \langle q,r \rangle \in Q \land \langle r,s \rangle \in S\}$

Intersection relations: $\forall X \exists I: I =\{\langle a,b \rangle| a \in X \land b \in X \land \exists c: c \in a \land c \in b \}$

Infinity: $\exists X: X=\{\alpha: \alpha \text { is finite von Neumann ordinal }\}$

Stages: $\forall \alpha: \text{ordinal}(\alpha) \to \exists X: X=V_\alpha$

Ceiling: $\exists \kappa : \forall \lambda > \kappa \ (|V_\lambda|=|V_\kappa|)$

All axioms except the last are true sentences of ZF, the last is abhorrent to ZF. The question is about the consistency of the above theory. The point is that if this theory is consistent, then it has an infinite domain, then one model of it admits an automorphism $j$ over it that shift ranks, take any ordinal $\kappa$ such that $j(\kappa) > \kappa$, then its easy to prove using Boffa model construction the theory $\sf NFU+ |Ur|=|Set|$, thereby interpreting $\sf NF$!

Seeing that Ceiling is very abhorrent to ZF, then there might be an obvious inconsistency for adding it to the above fragment of ZF, that I've overlooked?

Questions:

1. Is there a clear inconsistency with the above theory?

2. If $\sf NF$ is consistent, would it interpret the above theory?

3. If the above system is consistent, is there a direct argument for negating choice in it?