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][2], 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$][1]. 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)$$




  [1]: https://arxiv.org/ftp/arxiv/papers/2009/2009.03185.pdf
  [2]: https://randall-holmes.github.io/Papers/preserves4.pdf