Generalization principle in Infinitary language

Below is a question to mathoverflow, it is in latex, put it in any latex reader.

The following posting is along the general line of thought presented in this earlier posting titled ["Is it possible to derive the rules of set theory as transfers from the pure finite set world, and can we extend this further?"][1]. The idea is to simply view the constructive set theoretic rules (except infinity) as generalizations (transfers) of some rules coming from the standard hereditarily finite set world $V_\omega$. Informally the argument here is that any non-redundant formula $\phi$ in $V_\omega$ if $V_\omega$ satisfy existence of a set $\{y \mid \phi(y,\vec{v})\}$ for all $\vec{v}$, then this can be generalized over the whole set theoretic world $V$. The formal exposition of this principle shall be done in $\mathcal L(=,\in)_{\omega_1, \omega}$, since it can capture infinite sentences. 

First we add axioms to $\mathcal L(=,\in)_{\omega_1, \omega}$ enough to assure the existence of $V_\omega$, those are:

$\textbf{Extensionality: }  \forall z (z \in x \leftrightarrow z \in y) \to x=y$

$\textbf{Finite construction: } \bigwedge_{n \in \omega} \forall v_0..\forall v_n \exists x: x=\{v_0,..,v_n \} $

$\textbf{Define: } \operatorname {fin}(x)= x=\varnothing \bigvee_{n \in \omega} \exists v_0 .. \exists v_n: x=\{v_0,..,v_n\}$

$\textbf{Define: } x=\{y \mid \phi\} \equiv_{def} \forall y \, (y \in x \iff \phi)$

$\begin{align} \textbf{Infinity: }\\\exists x: x=\{y \mid & \ \operatorname {fin}(y) \ \land  \\& \neg[ \bigwedge_{n \in \omega} \exists v_0 .. \exists v_n: \bigwedge_{i \in n} (v_{i+1} \in v_i) \land v_0=y]\}\end{align}$

We name the above set $x$ as $V_\omega$ standing for the set of all true well founded hereditarily finite sets.

Second, we proceed with capturing non-redundancy of formulation, and stipulating the whole principle:

Let $\phi^{\psi_i}$ be an $\mathcal L(=,\in)_{\omega, \omega}$ formula in which formula $\psi_i$ occurs; with parameters among "$y,\vec{v}$" symbols.

$\psi_0, \psi_1, \psi_2,...$ are all of the formulas in $\mathcal L(=,\in) _{\omega, \omega}$ with appropriate parameters.

Let $\Phi^{\psi_i}$ be the set of all $\mathcal L_{\omega,\omega}$ formulas in which formula $\psi_i$ occurs, that are shorter than the formula $\phi^{\psi_i}$ in length (total number of symbols in a formula)

The principle is: 

$V_\omega \models\bigwedge_{i \in \omega} \bigwedge \neg \forall \vec{v} \forall y \, (\Phi^{\psi_i} \leftrightarrow \phi^{\psi_i}) \\ \underline {V_\omega \models \bigwedge_{i \in \omega}\forall \vec{v}\exists x :  x = \{y \mid \phi^{\psi_i}\}}\\ \bigwedge_{i \in \omega}\forall \vec{v} \exists x : x=\{y \mid \phi^{\psi_i}\} $

The above expression is saying that if no shorter formula than $\phi^{\psi_i}$ in which $\psi_i$ occur can be equivalent to $\phi^{\psi_i}$, and so $\phi^{\psi_i}$ expresses matters in $V_\omega$ in the shortest way; then it qualifies for the the generalization principle, which the last two lines of the above expression spells out. 

Examples: Let $\phi^{\psi_i}$ be "$(y=v_1 \lor y=v_2 \land (\psi_i \lor \neg \psi_i))$", this would prove pairing. If you replace $(\exists z \in v_0 (y \in z))$ or $(\forall z (z \in y \to z \in v_0))$ instead of what is before $\land$ in the above expression, then Union and Power would be enacted.

To prove Separation let $\phi^{\psi_i}$ be the formula $(y \in v_0 \land \psi_i(y))$. 

To prove Replacement take $\phi^{\psi_i}$ to be the formula $(\exists x \in v_0 \forall z (\psi_i(x,z) \leftrightarrow z=y))$.

This method relies essentially on redundancy to filter out pathological formulation captured by $V_\omega$ that cannot generalize beyond it, like for example the formula  "$y \text{ is infinite}$"

> Is there a clear counter-example to this principle?

  [1]: https://mathoverflow.net/q/298927/95347