Problem from Bonevac’s Book

[José Guilherme]

Problem from Bonevac’s Book

So there is this sequent from Bonevac’s book “Deduction” that I’m not quite seeing how to solve it. Looking at the exercise it appears to be obvious but I’m not being able to finish the formal demonstration.
The exercise is the following:

Vx (3yFxy -> VyFyx); 3x3yFxy; therefore VxVyFxy

Any comment would be most welcomed.

(I'm using "V" as the universal quantifier and "3" as the existential quantifier.)

 

[ksdhart2]

So what we have here is:

\(\displaystyle \forall x (\exists y F_{xy} \implies \forall y F_{yx})\)

\(\displaystyle \exists x \exists y F_{xy} \therefore \forall x \forall y F_{xy}\)

Is that correct?

 

[José Guilherme]

So what we have here is:

\(\displaystyle \forall x (\exists y F_{xy} \implies \forall y F_{yx})\)

\(\displaystyle \exists x \exists y F_{xy} \therefore \forall x \forall y F_{xy}\)

Is that correct?

Yes.
The first two propositions are the premisses and the third the conclusion that we have to show.