This question is related to a question Is this internalization of a bijection between a set and its powerset possible? lately posted to $\cal MO$, as well as to Can we have a bijection between a set and its powerset with the following properties? and 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 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 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, that is: $\forall S: (j^{-1} \circ f)[[S]]; (j^{-1} \circ f)^{-1}[[S]] \text { both exist}$.
