I need to complete the following proof using only primitive rules (the introduction and elimination rules for each connective and quantifier).
(∃x)(∀y)(Py ∨ Qx) ⊢ (∀y)Py ∨ (∃x)Qx
I've only been able to get this far:
1| (∃x)(∀y)(Py ∨ Qx) | Premise 2| a | (∀y)(Py ∨ Qa) | Assumption 3| | Pc ∨ Qa | ∀ elimination, 2 4| | (∃x)(Pc ∨ Qx) | ∃ introduction, 3 5| | e | Pc ∨ Qe | Assumption 6| | | ??? | ???
I can't figure out how to split the disjunction into its respective parts using only primitive rules.