How to prove that $\vdash \exists y \forall x P(x,y) \rightarrow \forall x \exists y P(x,y)$ with natural deduction in tree style

Question

I have built the following proof for $\vdash \exists y \forall x P(x,y) \rightarrow \forall x \exists y P(x,y)$ with natural deduction in tree style.

However, I am stuck in the middle of the problem... How can I conclude the right subtree of $∀_x P(x,y)$ ?

Answer 1

We start assuming $∃y∀xP(x,y)$ and we will derive $∀x∃yP(x,y)$. The result follows by $(\to \text I)$.

1. $∃y∀xP(x,y)$ --- premise

2. $∀xP(x,a)$ --- start sub-proof for $(\exists \text E)$: assumption [a] from 1), with $a$ new

3. $P(z,a)$ --- from 2) by $(\forall \text E)$

4. $∃yP(z,y)$ --- from 3) by $(\exists \text I)$.

5. $∀x∃yP(x,y)$ --- from 4) by $(\forall \text I)$: the proviso of the rule is satisfied because the variable we are "generalizing" is not free in the assumptions.

Having derived a formula with no occurrence of parameter used in assumption [a], the proviso for $(\exists \text E)$ is satisfied and we can close the sub-proof and discharge temporary assumption [a], concluding with:

6. $∀x∃yP(x,y)$ --- from 2)-5) and 1) by $(\exists \text E)$.