Is this predicate logic derivation valid? Could someone please be so kind as to check the validity of my predicate derivation? I am trying to prove that the set $\{(\forall x)\lnot(\exists y)Gxy,(\forall z)[Hz\implies(\exists z) Gzy],(\exists w)Hw\}$ is inconsistent, and have so conjured the following derivation:

*

*$(\forall x)\lnot(\exists y)Gxy$____Assumption

*$(\forall z)[Hz\implies(\exists z) Gzy]$____Assumption

*$(\exists w)Hw$____Assumption

*Hb____A/$\exists$E

*Hb $\implies$ ($\exists y$)Gby____2$\forall$E

*$(\exists y)$Gby____4,5$\implies$E

*Gba____A/$\exists$E

*$\lnot$Gab____A/$\lnot$E

*($\exists$ y)Gby____7$\exists$I

*$\lnot(\exists y)$Gby____1$\forall$E

*Gab____8-10$\lnot$E

*Gab____7-11$\exists$E

*($\exists y$)Gay____12$\exists$I

*($\exists y$)Gay____4$\exists$E

*$\lnot(\exists y)Gay$____1$\forall$E

I ask for this because I am still getting used to predicate proofs, and hence seek affirmation from the more proffesional. Thank you in advance.

Lines 9 and 10 are already a contradiction so I don't see why you need any of the subsequent lines.
