This question is related to a question lately posted to $\cal MO$. Similarly, we add one primitive unary partial function $``j"$ to the language of $\sf ZF$.

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

$\exists \alpha: \text{ limit} (\alpha) \land j: V_\alpha \to V_{\alpha +1} \land j \text{ is a bijection }$

$ \forall S: j[S]; j^{-1} [S] \text { both exist }$

$ \exists S: S= \{\{x,y\}\mid \exists z: z \in j(x) \land z \in j(y) \}$

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 Is this internalization of a bijection between a set and its powerset possible? lately posted to $\cal MO$. Similarly, we add one primitive unary partial function “$j$” to the language of $\sf ZF$.

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

$\exists \alpha: \text{ limit} (\alpha) \land j: V_\alpha \to V_{\alpha +1} \land \text{$j$ is a bijection }$

$ \forall S: \text {$j[S]$; $j^{-1} [S]$ both exist }$

$ \exists S: S= \{\{x,y\}\mid \exists z: z \in j(x) \land z \in j(y) \}$

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.