This question is related to a question https://mathoverflow.net/questions/405567/is-this-internalization-of-a-bijection-between-a-set-and-its-powerset-possible lately posted to $\cal MO$, as well as to https://mathoverflow.net/questions/406079/can-we-have-a-bijection-between-a-set-and-its-powerset-with-the-following-proper and https://mathoverflow.net/questions/405829/can-we-internalize-a-bijection-between-a-set-and-its-powerset-in-this-way, and especially the last where this post can be taken as a remedy of it since it was [proved](https://mathoverflow.net/a/405851) inconsistent. 

So similarly, we add two partial unary functions “$j$, $f$” to the language of $\sf ZF$. 

The question is about if we can add the following on top of axioms of $\sf ZF$ [$j,f$ not used in Replacement nor Separation]?

 $\exists \alpha: \text{ limit} (\alpha) \land j: V_{\alpha+1} \rightarrowtail V_\alpha   \land f: V_\alpha \equiv  \operatorname{rng}(j)  \\   \forall S: j[[S]]; j^{-1}[[S]]  \text { both exist }\\\forall S: f[S]; f^{-1} [S] \text { both exist }\\ \forall S \in V_\alpha \times V_\alpha: j(S)=f[S] $

Where: "$\equiv$" signifies "in bijection with", and $g[S]=\{g(x) \mid x \in S\},  g[[S]]= \{g[x] \mid x \in S\}$.

The first three conditions have already been proved consistent  (see [here][5] and from existence of external automorphisms); it's the addition of the fourth that is unsolved.


The rationale for this question is that if the above four conditions are met, then we'll have $j^{-1} \circ f: V_\alpha \to V_{\alpha+1}; x \mapsto j^{-1} (f(x)) $ being a *bijective* function satisfying the conditions of the first [posting][1], that is: $\forall S: (j^{-1} \circ f)[[S]]; (j^{-1} \circ f)^{-1}[[S]] \text { both exist}$.


  [1]: https://mathoverflow.net/questions/405567/is-this-internalization-of-a-bijection-between-a-set-and-its-powerset-possible?
  [2]: https://mathoverflow.net/questions/406079/can-we-have-a-bijection-between-a-set-and-its-powerset-with-the-following-proper?
  [3]: https://mathoverflow.net/questions/405829/can-we-internalize-a-bijection-between-a-set-and-its-powerset-in-this-way
  [4]: https://mathoverflow.net/questions/405829/can-we-internalize-a-bijection-between-a-set-and-its-powerset-in-this-way?answertab=active#tab-top
  [5]: https://mathoverflow.net/questions/405567/is-this-internalization-of-a-bijection-between-a-set-and-its-powerset-possible?#comment1039997_405567