How can I prove the following with natural deduction rules? $¬∀x∃yP(x,y) ⊢ ∃x∀y¬P(x,y)$

Question

I have been stuck with this problem for a long time, I tried reductio ad absurdum and I got the hypothesys $[¬∃x∀y¬P(x,y)]$, then I try to eliminate the negation of the premise, but I have to prove $∀x∃yP(x,y)$, and after using the introduction of universal quantifier rule, I go again with reductio ad absurdum, gaining a second hypothesis $[¬∃yP(x,y)]$. But at this point I have two hypothesis that contain negations of existencial quantifier, and I don't know how to use them constructively. I found some other similar questions, but all the answers given do not say which rules must be applied, and since I'm a beginner I didn't understand them.

Answer 1

You are doing this exactly right! You just have to derive $\forall y \neg P(x,y)$ from $\neg \exists y P(x,y)$

Now, I am not sure how your proof system defines the rule for $\forall$ Introduction ... in the system that I use you designate a 'fresh' constant to take the role of the arbitrary object from the domain. So this is what it looks like in my preferred system, called Fitch: