Given the premises in lines 1 and 2, I need to prove that $(\forall x)(\exists y)(Cx \rightarrow Axy)$.
- $(\exists x)(\forall y)Ayx \lor (\forall x)(\forall y)Bxy$
- $(\exists x)(\forall y)(Cy \rightarrow \neg Byx)\\ \qquad \qquad \qquad \therefore (\forall x)(\exists y)(Cx \rightarrow Axy)$
- $(\forall y)(Cy \rightarrow \neg Bya) \qquad$ (2, existential instance)
- $\neg (\forall x)(\exists y)(Cx \rightarrow Axy) \qquad$ (reductio ad absurdum)
- $\qquad (\exists x)\neg(\exists y)(Cx \rightarrow Axy) \qquad$ (4, quantifier negation)
- $\qquad (\exists x)(\forall y)\neg(Cx \rightarrow Axy) \qquad$ (5, quantifier negation)
- $\qquad (\forall y)\neg(Cb \rightarrow Aby) \qquad$ (6, existential instantiation)
- $\qquad \neg(Cb \rightarrow Aba) \qquad$ (7, universal instantiation)
- $\qquad \neg(\neg Cb \lor Aba) \qquad$ (8, material implication)
- $\qquad Cb \land \neg Aba \qquad$ (9, DeMorgan)
- $\qquad Cb \qquad$ (10, simplification)
- $\qquad \neg Aba \qquad$ (10, simplification)
If this is correct so far, then I need a contradiction. I can sort of "see" the contradiction in the first premise (which I haven't used yet). If I could instance the $Bxy$ on the RHS of line 1, I'd be done. But I can't instance that while the quantifier is not thee major operator. So, am I on the right track? If so, how do I separate line 1 so I can instance it?
Thanks.