Language (first order logic with equality "$=$" and membership "$\in$", and constant symbol "$j$")

Axiom: ID axioms +

There exists a set $A$, such that:

- Field: $\forall x \in j \ \exists a \in A \ \exists b \subseteq A (x=\langle a,b \rangle)$

$$\text{Define: } j(a)=b \iff \exists x \in j \ (x=\langle a,b \rangle)$$

Extensionality: $\forall a,b \in A \ [\forall x (x \in j(a) \leftrightarrow x \in j(b)) \rightarrow j(a)=j(b)]$

Functionality: $\forall a \in A \ \exists ! b \ (j(a)=b)$

Functional singletons: $\forall a \in A \ \exists b \ (b=\{a\} \wedge \exists k \in A (j(k)=b))$

Functional complements: $\forall a \in A \ \exists a' \ (a'=\{x \in A| x \not \in j(a)\} \wedge \exists k \in A (j(k)=a'))$

Functional binary union: $\forall a,b \in A \ \exists u \ (u=j(a) \cup j(b) \wedge \exists k \in A (j(k) = u))$

Functional set Union: $\forall x \in A \ \exists y \ ( y=\{z| \exists m \in j(x) (z \in j(m))\} \wedge \exists k \in A (j(k)=y) )$

Functional unordered relative products: $$\forall x,y \in A \ \exists z \\ (z=\{m| \exists k,l,a,b,c \ ( k \in j(x) \wedge l \in j(y) \wedge j(k)=\{a,c\} \wedge j(l)=\{c,b\} \wedge j(m)=\{a,b\}) \} \wedge \exists k \in A (j(k)=z))$$

Functional unordered intersection relation set: $$\exists x (x=\{y| \exists a,b,c,a^*,b^* (c \in a \wedge c \in b \wedge j(a^*)=a \wedge j(b^*)=b \wedge j(y)=\{a^*,b^*\})\}\wedge \exists k \in A (j(k)=x))$$

In English: this theory speaks of existence of a function $j$ that sends elements of a set $A$ to subsets of $A$ such that all singleton subsets of $A$ are in the range of $j$ and such that the range of $j$ is closed under Boolean union and complements relative to $A$, functional set union refer to existence of a set of all elements of subsets of $A$ that are $j$ coded by elements of a subset of $A$ present in the range of $j$, and that this set is $j$ coded by an element of $A$, functional intersectional relation set is the set of all $j$ codes of pairs of $j$ codes of intersecting subsets of $A$ that are present in the range of $j$, and that this set is in the range of $j$, while functional relative products is better be understood formally as written.

/Theory definition finished.

Then we get to interpret $NFU$, by defining a new membership relation $\epsilon$ as:

$y \ \epsilon \ x \leftrightarrow y \in j(x)$

over domain $A$.

If we additionally add that $j$ is an injection, i.e.:

$\forall a,b \ [j(a)=j(b) \rightarrow a=b]$

Then we get to interpret $NF$.

I don't see any clear argument that prevents $j$ from being an injective relation!

Question: is there any clear argument against $j$ being an injective function?

The idea behind this question is that if we use the usual Boffa model construction for NFU [click [here] (Page 5)], then take the downward rank moving automorphism $J$ (written as $j$ in the referred article, changed here to $J$ to avoid confusion with the above mentioned function $j$ of this posting), then take its converse from $V_{J(\alpha)+1}$ to $V_{\alpha+1}$ which would be an isomorphism, now take the Boolean union of it with the set $\{\langle x,\emptyset \rangle| x \in V_{\alpha} \setminus V_{J(\alpha)+1}\}$, then this union would be a witness of the above-mentioned function $j$, and this clearly interprets $NFU$ through relation $\epsilon$ defined above over domain $V_{\alpha}$. However this modified Boffa approach cannot be further modified here by letting $J$ be a bijection between $V_{\alpha +1}$ and $V_{\alpha}$ as to get $NF$, since $J$ is an isomorphism and sets are never isomorphic to their powers. Yet the point is that $j$ as presented in the posting here need not be an isomorphism!!! so this obstacle is removed, and hence the question posed here about whether $j$ can be an injective function while still fulfilling the above axioms.