Request for Help with Predicate Logic Proof 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.
 A: Well, we managed to figure out the proof. But it was pretty damn hard (for us). I don't really understand what the proof "says", and it's kind of all over the place (it's easier to understand if you color code the lines, which I can't do on here), but we think this is right.


*

*$(\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)

*$\qquad \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)

*$\qquad (\exists y)\neg Aya \qquad$ (12, existential generalization)

*$\qquad (\forall x)(\exists y)\neg Aya \qquad$ (13, universal generalization)

*$\qquad (\forall x)\neg(\forall y) Aya \qquad$ (14, quantifier negation)

*$\qquad \neg(\exists x)(\forall y) Aya \qquad$ (15, quantifier negation)

*$\qquad (Cb \rightarrow \neg Bba) \qquad$ (3, universal instantiation)

*$\qquad \neg Bba \qquad$ (11,17,modus ponens)

*$\qquad (\forall x)(\forall y)Bxy \qquad$ (1,16 disjunctive syllogism)

*$\qquad (\forall y)Bby \qquad$ (19, universal instantiation)

*$\qquad Bba \qquad$ (20, universal instantiation)

*$\qquad Bba \land \neg Bba \qquad$ (18,21, conjunction)

*$(\forall x)(\exists y)(Cx \rightarrow Axy) \qquad$ (4-22, reductio ad absurdum)

