Predicate Logic, Proof of validity . How to remove negation infront of existential quantifier?

I am stuck on how to get rid of the negation on "$\lnot \exists x~(P(x) \land R(x))$" in this particular case. I have a relative idea of going about this sentence , where first using 2nd premise eliminating the "$\exists x$" and then getting the "$P(x_0)$" and "$R(x_0)$" respectively, then after that using "$\forall x$" elimination to get "$P(x_0) \to (Q(x_0) \lor R(x_0))$", that then allows me to use the $P(x_0)$ from previous "$P(x_0) \land R(x_0)$" to eliminate the conditional connective that allows me to have 2 sub proofs to eliminate the disjunction. I can then do conditional introduction giving "$P(x_0) \to Q(x_0)$" needed and after that just introduction of $\forall x$ that gives me $\forall x~(P(x) \to Q(x))$ what I am looking for.

You have the right idea. However, you should start with assuming $P(x_0)$ for an otherwise arbitrary $x_0$, then eliminate the universal quantifier in the first premise to that witness, eliminate the conditional, and thence eliminate the resulting disjunction. (Since you have $P(x_0)$ and $Q(x_0)\lor R(x_0)$ at that point.)

In the left case, $Q(x_0)$ is trivially derived, while in the right case is where the magic happens. From $R(x_0)$ and the assumed $P(x_0)$ derive the existance of $P(x_0)\land R(x_0)$, that is $\exists x~(P(x)\land R(x)$, which would contradict the second premise. Explode that contradiction.

Then introduce a universal quantifier, deducing $\forall x~(P(x)\to Q(x))$ as desired.

$\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}}\fitch{~~1.~~\forall x~(P(x)\to(Q(x)\lor R(x))\hspace{10ex}\textsf{Premise}\\~~2.~~\neg\exists x~(P(x)\land R(x))\hspace{18ex}\textsf{Premise}}{\fitch{~~3.~~[x_0]\hspace{10ex}\textsf{Arbitrary Witness}}{\fitch{~~4.~~P(x_0)\hspace{10ex}\textsf{Assumption}}{~~5.~~P(x_0)\to(Q(x_0)\lor R(x_0))\hspace{10ex}\textsf{Universal Elimination}\\~~6.~~Q(x_0)\lor R(x_0)\hspace{10ex}\textsf{Conditional Elimination}\\\fitch{~~7.~~Q(x_0)\hspace{10ex}\textsf{Assumption (Left Case)}}{}\\~~8.~~Q(x_0)\to Q(x_0)\hspace{10ex}\textsf{Conditional Introduction}\\\fitch{~~9.~~R(x_0)\hspace{10ex}\textsf{Assumption (Right Case)}}{10.~~P(x_0)\land R(x_0)\hspace{10ex}\textsf{Conjunction Introduction}\\11.~~\exists x~(P(x)\land R(x))\ldots\hspace{10ex}\textsf{Existential Introduction}\\12.~~\bot\hspace{10ex}\textsf{Negation Elimination}\\13.~~Q(x_0)\hspace{10ex}\textsf{Explosion (Ex Falsum Quodlibet)}}\\14.~~R(x_0)\to Q(x_0)\hspace{10ex}\textsf{Conditional Introduction}\\15.~~Q(x_0)\hspace{10ex}\textsf{Disjunction Elimination}}\\16.~~P(x_0)\to Q(x_0)\hspace{10ex}\textsf{Conditional Introduction}}\\17.~~\forall x~(P(x)\to Q(x))\hspace{10ex}\textsf{Universal Introduction}}$

Basic idea: Assume P(a). Deduce Q(a) within the scope of P(a).

For a hint on getting rid of the negation note that existential introduction doesn't have any restrictions, does it?

More detail:

Assume (P(a)$\land$R(a)), where 'a' is a constant. Then you can get a contradiction (hint: use existential introduction). So, you can infer $\lnot$(P(a)$\land$R(a)). But, then 'a' will appear and not appear anywhere else in assumptions made. Thus, you'll have the ability to use universal introduction, to have ∀x$\lnot$(P(x)$\land$R(x)). Then using a De Morgan law you have ∀x($\lnot$P(x)$\lor$$\lnot$R(x)).

Then assume P(a). By universal elimination you can infer ($\lnot$P(a)$\lor$$\lnot$R(a)). So, you can manage to get to $\lnot$R(a). Also, derive (Q(a)$\lor$R(a)) by using the first premise and P(a). So, you can then derive Q(a).

Then discharge P(a) yielding (P(a)$\rightarrow$Q(a)). And note that 'a' doesn't appear in any assumptions still in effect for the last step.