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 \} $

Now if $F$ happens to be an *isomorphism on $\in$*, 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$ that is not an isomorphism on $\in$?

> 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