This question is related to a question 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 consistent, it's the addition of the last condtion that is unsolved?

This question is related to a question 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 consistent, it's the addition of the last condtion that is unsolved?

This question is related to a question 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 have already been proved consistent, it's the addition of the last condtion that is unsolved?

This question is related to a question 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 consistent, it's the addition of the last condtion that is unsolved?