How to eliminate implications with quantifiers

Question

I'm reading some stuffs on the conversion of a FOL sentence to CNF form. However, I'm stuck with this problem: why should this

$$\forall x [\forall y Animal(y) \Rightarrow Loves(x,y)] \Rightarrow [\exists y Loves(y,x)]$$

be equal to this $$\forall x [\neg \forall y \neg Animal(y) \lor Loves(x,y)] \lor [\exists y Loves(y,x)]$$

? I know that $\alpha \Rightarrow \beta$ is equivalent to $\neg \alpha \lor \beta$, but I can't figure out how this equivalence was applied at the first sentence.

---

EDIT

Ok, it seems that Wikipedia has the same example, but a different (I think) soultion at this link. The step by step simplification looks like this.

$$\forall x [\forall y Animal(y) \Rightarrow Loves(x,y)] \Rightarrow [\exists y Loves(y,x)]$$ $$\forall x [\forall y \neg Animal(y) \lor Loves(x,y)] \Rightarrow [\exists y Loves(y,x)]$$ $$\forall x \neg[\forall y \neg Animal(y) \lor Loves(x,y)] \lor [\exists y Loves(y,x)]$$

Then, it continues moving the $\neg$ inward in this way. $$\forall x [\exists y \neg (\neg Animal(y) \lor Loves(x,y))] \lor [\exists y Loves(y,x)]$$ but it seems quite different from the result of my example. So, is the formula shown on my book wrong?

Answer 1

It might help to see what they did if you add some extra brackets. Note that: \begin{align*} &\forall x \, \left[ \forall y \, [\textsf{Animal}(y) \to \textsf{Loves}(x, y)] \to \exists y \, \textsf{Loves}(y, x) \right] \\ &\equiv \forall x \, \left[ \forall y \, [\neg \textsf{Animal}(y) \lor \textsf{Loves}(x, y)] \to \exists y \, \textsf{Loves}(y, x) \right] \\ &\equiv \forall x \, \left[\neg \forall y \, [\neg \textsf{Animal}(y) \lor \textsf{Loves}(x, y)] \lor \exists y \, \textsf{Loves}(y, x) \right] \\ \end{align*}

Answer 2

First, we have to "restore" the missing parentheses :

∀x[∀y(Animal(y)⇒Loves(x,y)) ⇒ ∃yLoves(y,x)]

then apply the "transformtion to the "inner" ⇒ :

∀x[∀y(¬ Animal(y) ∨ Loves(x,y)) ⇒ ∃yLoves(y,x)]

and then to the "outer" one :

∀x[¬∀y(¬ Animal(y) ∨ Loves(x,y)) ∨ ∃yLoves(y,x)].