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$

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

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

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|)$

Where $\bigcup, \mathcal P, V_\alpha,..$ all have their usual conventional meaning.

All axioms except the last are true sentences of ZF, but the last is abhorrent to ZF. The idea is that we don't have full separation, so that Cantor's theorem may be blocked. 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 external automorphism $j$ over it that shift ranks, take any ceiling ordinal $\kappa$ such that $j(\kappa) > \kappa$, then its easy to interpret 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. Is the above system interpretable in $\sf NF$, or even in some known extension of $\sf NF$?

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