Add a primitive partial unary function symbol $F$ to the first order language of set theory.

Working in Zermelo (Separation restricted to the language of set theory), add the following axioms:

$F$ function: $\exists X ( F: \mathcal P(X) \longrightarrow X, F \text { is injective} )$

Forward copying:$ \forall A \exists B: B = \{ \{ F(n)| n \in m \}| m \in A \} $

Backward copying: $ \forall A \exists B: B = \{ \{ n| F(n) \in m \}| m \in A \} $

Note: It needs to be emphasized that $F$ is an external function, and that it cannot be used in instances of separation. The proof that such an injective $F$ can exist can be seen from Boffa model construction for NFU. See here page 5, only restrict the automorphism $j$ to $V_{\alpha +1}$, and you get our $F$ where $V_\alpha$ would witness $X$ here.

Now if the graph of $F$ happens to be an isomorphism on $\in$ [between $dom(F)$ and $Range(F)$], then $F$ cannot be bijective! Since the parity of the set of all ordinals in $\mathcal P(X)$ is different from that in $X$. Hence the following questions:

Is there an example of $F$ whose graph is not an isomorphism on $\in$ between its domain and range?

If so, then is it the case that the qualifications of $F$ in the above system are still enough as to forbid $F$ from being a bijection?

The rationale beyond the above question is that if there is no clear argument against $F$ being bijective, then this might entail opening the door for a possible proof of $\sf Con(NF)$, as $F$ being bijective would easily interpret a finite axiomatization of $\sf NF$. The interpretation is over $\mathcal P^{-1} (dom(F))$ using a new membership relation $\in^F$ defined as: $$ y \in^F x \iff y \in F^{-1}(x)$$