This question is related to a [question][1] lately posted to $\cal MO$, as well as to [this][2] and [that][3] question, and especially the last where this post can be taken as a remedy of it since it was [proved][4] incconsistent. 

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  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 +1}: j(S)=f[S] $

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

The first three conditions have already been [proved][5] consistent, it's the addition of the fourth that is unsolved?


  [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