How to complete the follow natural deduction in bottom-up method I'm confuse about how to proceed with the follow natural deduction. I'm following the bottom-up method. Any suggestion will be welcome, but I think it's almost finished.
hypotheses found: [∀x∃y ¬α(x, y)] , [∃x∀yα(x, y)] , [∀yα(x, y)]
____________________________
[∃x∀yα(x, y)]       ⊥
____________________________e∃
              ⊥
____________________________I¬
         ¬∃x∀yα(x, y)
____________________________I→
∀x∃y ¬α(x, y) → ¬∃x∀yα(x, y)

 A: What you did goes in the right direction!
Following up your attempt, you need to prove a contradiction $\bot$, and the way to prove a contradiction (thanks to the rule $\lnot_E$) is to prove both a formula $\varphi$ and its negation $\lnot \varphi$, using the hypotheses you have.
In your hypotheses, you have $\forall y \,\alpha (x,y)$ and $\forall x \exists y \,\lnot \alpha(x,y)$, thus it would be enough to find a way to eliminate the quantifiers to make the contradiction $\alpha (x,y)$ and $\lnot \alpha (x,y)$ emerge.
Taking into account the informal idea above, a derivation in natural deduction for the formula $\forall x \exists y \, \lnot \alpha (x,y) \to \lnot \exists x \forall y \, \alpha (x,y)$ should have the following structure:
\begin{equation}
\dfrac{[\exists x \forall y \, \alpha (x,y)]^\circ \qquad \dfrac{\overset{\vdots \, ?}{\lnot \alpha(x,y)} \qquad \dfrac{[\forall y \, \alpha(x,y)]^\bullet}{\alpha(x,y)}\forall_E}{\bot}\lnot_E }{\dfrac{\dfrac{\bot}{\lnot \exists x \forall y \, \alpha (x,y)}\lnot_I^\circ}{\forall x \exists y \, \lnot \alpha (x,y) \to \lnot \exists x \forall y \, \alpha (x,y)}\to_I^*}\exists_E^\bullet
\end{equation}
Now a difficult arises: from the hypothesis $\forall x \exists  y \, \lnot \alpha(x,y)$ you get (reading the derivation top-down) $\exists y \, \lnot \alpha(x,y)$ via the rule $\forall_E$, but from $\exists y \, \lnot \alpha(x,y)$ how can you get $\lnot \alpha(x,y)$? (See the vertical dots in the pseudo-derivation above.)
The rule $\exists_E$ is a bit tricky, and it does not allow the variable $y$ to be free in its conclusion, so $\lnot \alpha (x,y)$ cannot be the conclusion of the rule $\exists_E$ we use to eliminate the existential quantifier from $\exists y \, \lnot \alpha(x,y)$. What can you do?
The solution is easy: you internalize the subderivation with conclusion $\bot$ (the conclusion of the rule $\lnot_E$ in the pseudo-derivation above) inside the subderivation we use to eliminate the existential quantifier from $\exists y \, \lnot \alpha(x,y)$. Therefore, a derivation in natural deduction for the formula $\forall x \exists y \, \lnot \alpha (x,y) \to \lnot \exists x \forall y \, \alpha (x,y)$ is the following:
\begin{equation}
\dfrac
{
  [\exists x \forall y \, \alpha (x,y)]^\circ \qquad 
  \dfrac
  {
    \dfrac
    {[\forall x \exists y \, \lnot \alpha(x,y)]^*}
    {\exists y \, \lnot \alpha(x,y)}
    \forall_E
    \qquad
    \dfrac
    {
      [\lnot \alpha(x,y)]^\#
      \qquad 
      \dfrac
      {[\forall y \, \alpha(x,y)]^\bullet}
      {\alpha(x,y)}
      \forall_E
    }
    {\bot}
    \lnot_E}
  {\bot}
  \exists_E^\#
}
{
  \dfrac
  { 
    \dfrac
    {\bot}
    {\lnot \exists x \forall y \, \alpha (x,y)}
    \lnot_I^\circ
  }
  {
    \forall x \exists y \, \lnot \alpha (x,y) \to \lnot \exists x \forall y \, \alpha (x,y)
  }
  \to_I^*
}
\exists_E^\bullet
\end{equation}
The symbols $*$, $\#$, $\circ$ and $\bullet$ mark when the hypotheses have been discharged.
