How to prove the tautology $\neg \forall{x} \exists{y} (Py \wedge \neg Px)$?

I've been beating my head trying to prove the following tautology for some time:

$$\therefore \neg \forall{x} \exists{y} (Py \wedge \neg Px)$$

I think there's some tricky intermediate step that I'm missing. Any help would be appreciated.

-

Let's start from the equivalent form $$\exists x \big( \forall y (\lnot Py \vee Px) \big),$$ where I've added a set of brackets for clarity. The inner statement contains a disjunction where one of the sentences is independent of $y$; therefore we can move that sentence out of the scope of the quantifier: $$\exists x \big( Px \vee \forall y (\lnot Py) \big).$$ Now we again have a disjunction where the second sentence is independent of $x$, so we separate it in a similar way: $$\exists x (Px) \vee \forall y (\lnot Py).$$ This is clearly a tautology, after changing the second half to the equivalent $\lnot\exists x(Px)$.
Let's rewrite it explicitely so the tautological character of the sentence can be easily seen. $$\exists_x \forall_y \, \neg P(y) \vee P(x)$$ It simply says that either ($\exists_x P(x)$) or ($\forall_y \,\neg P(y)$) holds for each formula P.
Refolmulated statement is of the form $\neg q \vee q$ for $\forall_x P(x)$ replaced by $q$ and I think you could take it as an axiom (called law of excluded middle). –  Kuba Helsztyński Jul 24 '12 at 5:30