Doubts finding a Prenex normal form $ \exists x\alpha\vee\exists y\beta=\exists x(\alpha\vee\beta) $ I'm getting troubles when finding a Prenex Normal form of a formula at First-order logic exercises... and ask for help: 
First, I know the equivalence: 
$$ \forall x
 \alpha\wedge\forall y\beta=\forall x(\alpha\wedge\beta)
 $$
and 
$$ \exists x\alpha\vee\exists y\beta=\exists x(\alpha\vee\beta)
 $$
So.. I need to find a Prenex Normal Form of: 
$\alpha:=\forall[\exists y(P(y)\wedge Q(x,y))]\vee\forall y[\forall zQ(y,f(z))\rightarrow P(y)] $  with as few quantifiers as possible and I have:
$$ \alpha:=\forall[\exists y(P(y)\wedge Q(x,y))]\vee\forall y[\forall zQ(y,f(z))\rightarrow P(y)] $$
$$ \alpha\equiv\forall x\exists y(P(y)\wedge Q(x,y))\vee\forall y(
 \text ¬\forall zQ(y,f(z))\vee P(y)) $$
$$ \alpha\equiv\forall x\exists y(P(y)\wedge Q(x,y))\vee\forall y(
 \exists zQ(y,f(z))\vee P(y)) $$
$$ \alpha\equiv\forall x\exists y(P(y)\wedge Q(x,y))\vee\forall y\exists z(
 Q(y,f(z))\vee P(y)) $$
but I'm not sure if I can say that: 
$$ \alpha\equiv\forall x\forall y\exists z[(P(z)\wedge Q(x,z))\vee(
 Q(y,f(z))\vee P(y))]
 $$
or something like that in order to remove a quantifier...
Any idea (?) thank you so much! 
 A: You already have this much
$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \rangle  \lor \forall \langle y,~ \forall \langle z,~ Qy(fz)\rangle  \implies Py\rangle $$
$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \rangle  \lor \forall \langle y,~ \lnot \forall \langle z,~ Qy(fz)\rangle  \lor Py\rangle $$
$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \rangle  \lor \forall \langle y,~ \exists \langle z,~ \lnot Qy(fz)\rangle  \lor Py\rangle $$
$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \rangle  \lor \forall \langle y,~ \exists \langle z,~ \lnot Qy(fz) \lor Py\rangle \rangle $$
Recommanded next step is
$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle  \lor \forall \langle y,~ \exists \langle z,~ \lnot Qy(fz) \lor Py\rangle \rangle \rangle  $$
$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle  \lor \forall \langle w,~ \exists \langle z,~ \lnot Qw(fz) \lor Pw\rangle \rangle \rangle  $$
$$\forall \langle x,~ \forall \langle w,~ \exists \langle y,~ Py \land Qxy\rangle  \lor \exists \langle z,~ \lnot Qw(fz) \lor Pw\rangle \rangle \rangle  $$
Now the $y$ and $z$ can be combined into something like $s$:
$$\forall \langle x,~ \forall \langle w,~ \exists \langle s,~ (Ps \land Qxs) \lor (\lnot Qw(fs) \lor Pw)\rangle \rangle \rangle  $$
