Formal proof of $\exists x \forall y P(x,y) \implies \forall y \exists x P(x,y)$

Question

Say that the variables $x,y$ of a predicate $P$ are taken from some non-empty set. It is clear that the following statement is true. How should a formal proof look?

$$\exists x \forall y P(x,y) \implies \forall y \exists x P(x,y)$$

Answer 1

To formally prove a logical implication you need to show that whenever $M$ is a structure for the language including the relevant symbols, if $M\models\exists x\forall yP(x,y)$, then $M\models\forall y\exists xP(x,y)$.

In order to prove that, one has to begin with taking such $M$ then deconstruct the definition of the assumption, $M\models\exists x\forall yP(x,y)$, and reconstruct that $M\models\forall y\exists xP(x,y)$ is true.

---

If by $\implies$ you actually meant $\rightarrow$, the connective whose truth table is $p\rightarrow q$ is false if and only if $p$ is true and $q$ is false; then the proof should begin with a structure $M$ for the language, and you need to show that $M$ satisfies this statement.

The proof is in fact quite similar to the above one, in this aspect.