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$. Here, 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 \to V\_{\alpha +1} \land f: V\_\alpha \to V\_\alpha \land j,f \text{ are bijections } \\ \forall S: j[S]; j^{-1} [S] \text { both exist } \\ \forall S \in V\_\alpha: j(S)=f[S] $


Where: $g[S]=\{g(x) \mid x \in S\}$


The first two conditions have already been [proved](https://mathoverflow.net/questions/405567/is-this-internalization-of-a-bijection-between-a-set-and-its-powerset-possible?#comment1039997_405567) consistent, it's the addition of the last condtion that is unsolved?



Can we internalize a bijection between a set and its powerset in this way?
The above theory is inconsistent. Since j is surjective, there is an x∈ with jx=. Then f[x]=. Therefore x=, since f is a bijection. But is not an element of .


