Is there anything against this function j being injective?

Question

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

Axiom: ID axioms +

There exists a set $A$, such that:

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

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

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

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

5. 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'))$

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

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

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

9. 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.

Answer 1

Once you have such a $j$ you can make another one that is not injective: take a bijection $b:A\to A\times A$ and the projection $\pi:A\times A\to A$ onto the first coordinate. Then the composition $j\circ\pi\circ b$ is far from injective and it also satisfies your conditions.

On the other hand: by means of a well-order $\prec$ of $A$ in type $|A|$ you can turn any non-injective $j$ into an injective one. From $\prec$ define $B=\{x\in A:(\forall y\in A)(j(y)=j(x)\Rightarrow x\preceq y)\}$, now the restriction of $j$ to $B$ is injective and $j[B]=j[A]$; let $b:A\to B$ be the unique order-preserving bijection defined by $b(x)=\min B\setminus\{b(y):y\prec x\}$. Then the composition $j \circ b$ would be an injection that satisfy all properties 1--9.