Help with Logic proof writing?

Question

How would one derive (or show that you cannot) $$Q \lor (\exists y)Gy$$ From $$(\exists x)(Q \lor Gx) (1)$$

I think I have a preliminary approach:

Assume $a$ satisfies (1). Then $$Q \lor Ga$$. Then from existential generalization, we can get $$Q \lor (\exists y) Gy$$ My problem is, is that I'm not sure I've actually discharged my assumption for $Ga$.

Answer 1

1) $\exists x \ (Q \lor Gx)$ --- premise

2) $Q \lor Ga$ --- assumed from 1) for $\exists$-elim

But now, we cannot apply $\exists$-intro to $Q \lor Ga$ to get $Q \lor (\exists y)Gy$.

We have first to "unpack" the disjunction :

3) $Q$ --- assumed [a] from 2) for $\lor$-elim

4) $Q \lor (\exists y)Gy$ --- from 3) by $\lor$-intro

5) the same assuming [b] $Ga$ from 2)

6) $Q \lor (\exists y)Gy$ --- from 2) and 3)-4) and 5) by $\lor$-elim, discharging both temporary assumpions [a] and [b]

With 6), we can discharge also the initial assumption : $Q \lor Ga$ used for $\exists$-elim.