Using the Fitch application and only Intro and Elim rules (& REIT if necessary), prove that
$$forall x forall y (P(x) implies Q(y)) iff (exists x P(x) implies forall y Q(y))$$
is a logical truth (i.e. prove it from no premises)
I am attaching a screenshot of my work so far, please give me feedback and/or assistance so that I can fix or finish this proof. I am currently stuck and don’t know if what I did is right or not because I don’t know what to do next. Any feedback is appreciated.