Negation of the semantics of the Until operator in LTL

Question

I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to:

$\phi R \psi \equiv \neg(\neg\phi U \neg \psi)$

But when trying to get from the semantic definition of the Until operator to the semantic definition of the Release operator by negation I get stuck part way. Specifically, I get stuck trying to negate a $\forall j < i$ expression as I will show below.

So the semantic definition of Until:

$\pi \models \phi U \psi \iff \exists i \geq0, \pi[i] \models \psi \land \forall j\leq i-1, \pi[j]\models \phi$

Putting the negations in:

$\pi \models \neg(\neg\phi U \neg\psi) \iff \neg(\exists i \geq0, \pi[i] \models \neg\psi \land \forall j< i, \pi[j]\models \neg\phi)$

$\iff \forall i \geq 0, \neg(\pi[i]\models\neg\psi)\lor \neg(\forall j < i,\pi[j]\models\neg\phi)$

$\iff \forall i \geq 0, (\pi[i]\models\psi)\lor (\exists j < i,\pi[j]\models\phi)$

In words, I am ending up with globally $\psi$ or globally there always exists some predecessor that satisfies $\phi$. Which cannot be correct as $\pi[j]$ is not defined when $i=0$.

The semantic definition for the release operator that I was aiming for is:

$\pi \models \phi R\psi \iff (\exists i\geq 0, \pi[i]\models\phi \land \forall j\leq i, \pi[j]\models\psi)\lor (\forall k \geq 0, \pi[k] \models \psi)$

So I have part of the expression correct ($\forall k \geq 0, \pi[k] \models \psi \equiv \forall i \geq 0, (\pi[i]\models\psi)$), but I am really stumped about how to get the second part or where I went wrong.

Any help enlightening me is greatly appreciated!

Thanks!