Ubiquity beyond infinity, transitive closure and the recursion theorem?

Question

I am considering a Principle of Ubiquity, expressed as follows - for a class theory where precisely the elements are sets - with the aid of set abstracts:

For $\alpha(y,z)$ a first order condition so that $\forall y(\exists w(y\in w)\to \exists w (\{z|\alpha(y,z)\}\in w))$:

$\forall v(\exists t (v\in t)\to\exists t(\{w|\forall x(v\in x\wedge \forall y(y\in x\to \{z|\alpha(y,z)\}\in x)\to w\in x)\}\in t))$

The set abstracts can be eliminated with the following Mendelsonian abstraction schema:

$\forall x(x\in \{x|\alpha\}\leftrightarrow\exists y(x\in y)\wedge\alpha)$

It is immediate that we get a theorem of infinity, as well as the least transitive closure of all sets; moreover, several further instances of replacement will hold, though with countable co-finality.

May Z with Ubiquity, instead of just the Axiom of Infinity, justify the Recursion Theorem?

Answer 1

The answer seems to be affirmative.

Let an adapted version of ubiquity be as follows:

For $\alpha(y,z)$ a functional first order condition so that

$\forall y(\exists w(y\in w)\to \exists w(\{z|\alpha(y,z)\}\in w))$:

$\forall v(\exists w(v\in w)\to\exists w(\{u|\forall x(v\in x\wedge \forall n \forall y(((n,y)\in x\to (n+1,\{z|\alpha(n,z)\})\in x))\to u\in x)\}\in w))$

Let $v=(0,X)$

Let $F=\{u|\forall x(v\in x\wedge \forall n \forall y(((n,y)\in x\to (n+1,\{z|\alpha(n,z)\})\in x))\to u\in x)\}$

We see that $(0,X)\in F$.

Moreover, for any $n$ and $y$, if $(n,y)\in F$ then $(n+1,\{z|\alpha(n,z)\}\in F)$

We see that function F is the least class with these properties, and from the assumption of Infinitude that F is a set.

As F is a set, Mendelsonian abstraction gives us that

$(0,X)\in F\wedge ((n+1,y)\in F\leftrightarrow\exists w((n,w)\in F\wedge \forall u(u\in w\leftrightarrow \alpha (n,u)))$

Am I done?

Edit: Unsurprisingly, Replacement entails Ubiquity.