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