This exercise is from section 3.4 of the textbook Mathematical Logic by Ebbinghaus. It just asks
Show $\exists x \forall y \phi \models \forall y \exists x \phi$
I do have a basic idea of how to go about it, but I'm not comfortable with the fact that it involves the manipulation of English, because some of the definitions themselves use English (namely definition 3.3.2, which establishes the satisfaction relation). I looked at some other proofs online (not using the same book) and they all seemed to be more convincing than mine, because they all justify every step using theorems, which weren't covered in this book.
I labelled the steps so it's easier to read:
Let $\mathfrak J$ be an interpretation such that $\mathfrak J \models \exists x \forall y \phi$.
$\mathfrak J \models \exists x \forall y \phi$ iff there exists an $a \in A$ (the domain) such that $\mathfrak J \frac{a}{x} \models \forall y \phi$.
$\mathfrak J \frac{a}{x} \models \forall y \phi$ iff for all $a' \in A$, $\mathfrak J \frac{a}{x}\frac{a'}{y} \models \phi$.
Hence, $\mathfrak J \models \exists x \forall y \phi$ iff there exists an $a \in A$ such that for all $a' \in A$, $\mathfrak J \frac{a}{x}\frac{a'}{y} \models \phi$.
(icky part) $\mathfrak J \models \exists x \forall y \phi$ iff for all $a' \in A$, there exists an $a \in A$ such that $\mathfrak J \frac{a}{x}\frac{a'}{y} \models \phi$.
One can easily show that $\mathfrak J \frac{a}{x}\frac{a'}{y} = \mathfrak J \frac{a'}{y}\frac{a}{x}$ (this will be justified in the actual proof).
Thus, $\mathfrak J \models \exists x \forall y \phi$ iff for all $a' \in A$, there exists an $a \in A$ such that $\mathfrak J \frac{a'}{y}\frac{a}{x} \models \phi$.
$\mathfrak J \models \exists x \forall y \phi$ iff for all $a' \in A$, $\mathfrak J \frac{a'}{y} \models \exists x \phi$
$\mathfrak J \models \exists x \forall y \phi$ iff $\mathfrak J \models \forall y \exists x \phi$
Now that I think about it, I think that the "iff" should be changed to an "if" around step 5 but I'm too tired at the moment to edit it. Anyways, I don't like this proof sketch because it looks ugly, and it involves the manipulation of English, which I would like to avoid at all costs. However I don't know how to go about this by avoiding English. Can anyone else familiar with the book help me out here? Thanks!
So, the inference from 4 to 5 in your example is not correct. You can conclude that $\exists \forall \implies \forall \exists$, even at the meta level, but it doesn't change the meaning of the syntax.
Your conclusion 9 is also NOT CORRECT. $\forall \exists$ does not entail $\exists \forall$.
To see this, consider the following argument.
Here's a way to solve it by taking a detour through existential second-order logic, for the nice syntax. You don't actually need it. I'm only using it here because it lets me keep arguments about reordering quantifiers out of the meta level to some degree.
This is also a proof by contrapositive. I assume the negation of the conclusion and prove the negation of the hypothesis.
$ [\exists x][\forall y](\varphi(x, y)) \models [\forall y][\exists x](\varphi(x, y))$ means that, for all $M, v$ such that $M, v \models [\exists x][\forall y](\varphi(x, y))$, it holds that $M, v \models [\forall y][\exists x](\varphi(x, y))$.
Suppose by way of contrapositive that:
$$ M, v \not\models [\forall y][\exists x](\varphi(x, y)) $$
Thus
$$ M, v \models [\exists y][\forall x](\lnot \varphi(x, y)) $$
Next, we note that we can choose as an interpretation of the new bound function symbol $f$ the function that ignores its argument and returns the former interpretation of $y$.
$$ M, v \models [\exists f][\forall x](\lnot \varphi(x, f(x)))$$
However, if there is a function $f$ such that for all $x$ the negation of $\varphi$ holds, then for every $x$ there exists a $y$ such that the negation of $\varphi$ holds.
$$ M, v \models [\forall x][\exists y](\lnot \varphi(x, y) $$
And thus, as desired:
$$ M, v \not\models [\exists x][\forall y](\varphi(x, y)) $$