Problem with transforming a formula to Prenex CNF

Question

I've been trying to transform the following formula all day long with no avail:

$\lnot[\forall x \exists y F(u,x,y) \to \exists x (\lnot \forall y G(y,v) \to H(x))]$

the answer sheet gives us the solution but not the steps, here it is:

∀x∃y∃z[F(u, x, y) ∧ ¬G(z, v) ∧ ¬H(x))]

I can't seem to find a way to properly reach that conclusion. I'll transcribe one of my tries in painstaking detail and I'd be immensely grateful if someone could point out where I made a mistake:

1) $\lnot[\forall x \exists y F(u,x,y) \to \exists x (\lnot \forall y G(y,v) \to H(x))]$

2) $\lnot[\lnot \forall x \exists y F(u,x,y) \lor \exists x (\lnot \forall y G(y,v) \to H(x))]$

3) $\lnot[\exists x \forall y \lnot F(u,x,y) \lor \exists x (\lnot \forall y G(y,v) \to H(x))]$

4) $\lnot[\exists x \forall y \lnot F(u,x,y) \lor \exists x (\lnot \lnot \forall y G(y,v) \lor H(x))]$

5) $\lnot[\exists x \forall y \lnot F(u,x,y) \lor \exists x (\forall y G(y,v) \lor H(x))]$

6) $\lnot\exists x \forall y \lnot F(u,x,y) \land \lnot \exists x (\forall y G(y,v) \lor H(x))$

7) $\forall x \exists y F(u,x,y) \land \lnot \exists x (\forall y G(y,v) \lor H(x))$

8) $\forall x \exists y F(u,x,y) \land \forall x \lnot (\forall y G(y,v) \lor H(x))$

9) $\forall x \exists y F(u,x,y) \land \forall x \lnot \forall y G(y,v) \land H(x))$

10) $\forall x \exists y F(u,x,y) \land \forall x \exists y G(y,v) \land H(x))$

After this I simply gave up because I saw that no matter how I distributed the quantifier I wouldn't be able to reach the provided answer.

Answer 1

You should have the following.   Check for where you dropped negation (9-10).

10. $(\forall x~\exists y~F(u,x,y)) \land (\forall x~((\exists y~\lnot G(y,v)) \land \lnot H(x)))$

Now the universal distributes over conjunction: $(\forall a~\phi)\land(\forall a~\psi)\iff (\forall a~(\phi\land \psi))$

11. $\phantom{\forall x~(\exists y~F(u,x,y) \land ((\exists y~\lnot G(y,v)) \land \lnot H(x)))}$

However Existential does not; therefore we must use alpha substitution in one of the two existentials.   Substituting in the second will lead to the target.

12. $\phantom{\forall x~(\exists y~F(u,x,y) \land ((\exists z~\lnot G(z,v)) \land \lnot H(x)))}$

You can there by use that $\psi\land(\exists a~\phi)\equiv \exists a~(\psi\land\phi)$ if $a$ is not free in $\psi$ (and the universe is not-empty).

13. ${\forall x~\exists y~\exists z~(F(u,x,y) \land \lnot~G(z,v) \land \lnot H(x))}$