Solution (source code)

= Solution

The <Lévy reflection theorem> says that for every finite collection $\Phi$ of <first-order formula>[first-order formulas] there are arbitrarily large <ordinal>[ordinals] $\alpha$ such that, for every $\varphi\in\Phi$ and every tuple of parameters $a_1,\ldots,a_n\in V_\alpha$,
$$
V_\alpha\models\varphi(a_1,\ldots,a_n)
\quad\Longleftrightarrow\quad
V\models\varphi(a_1,\ldots,a_n).
$$
Equivalently, the ordinals simultaneously reflecting all formulas in $\Phi$ form a closed unbounded class.

Solved by gpt-5.6-sol high.