Hints and/or help needed for axiomatic deduction

Question

Proof: $\forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay) \vdash \forall x (Rxx \rightarrow \neg Ax)$

Axioma schema's that can be used:

1 $(\forall x(\varphi \rightarrow \psi)) \rightarrow (\forall x \varphi \rightarrow \forall x \psi)$
2 $\varphi \rightarrow \forall x \varphi$ ($x$ not free in $\varphi$)
3 $\forall x \varphi \rightarrow [t/x]\varphi$ (only if the term $t$ is free for $x$ in $\varphi$)
a $\varphi \rightarrow (\psi \rightarrow \varphi)$
b $\varphi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi)\rightarrow (\varphi \rightarrow \chi))$
c $(\neg \varphi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \varphi)$

And Modus Ponens for deductions.

What I got so far:

$\Sigma = \{\forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay)\}$

1 $\Sigma \vdash \forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay)$ assumption
2 $\vdash \forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay) \rightarrow \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay)$ Axiom schema 3
3 $\Sigma \vdash \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay)$ MP, 1, 2
4 $\vdash \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay) \rightarrow (Az \rightarrow Rzz) \rightarrow \neg Az$ Axiom schema 3
5 $\Sigma \vdash (Az \rightarrow Rzz) \rightarrow \neg Az$ MP, 3, 4

And here is where I get stuck. I'm thinking maybe something like:

6 $Az \rightarrow Rzz \vdash Az \rightarrow Rzz$ auxiliary assumption
7 $\Sigma, Az \rightarrow Rzz \vdash \neg Az$ MP, 5, 6
8 $\vdash \neg Az \rightarrow (\neg Rzz \rightarrow \neg Az)$ Axiom schema a
9 $\Sigma, Az \rightarrow Rzz \vdash \neg Rzz \rightarrow \neg Az$ MP, 7, 8

But then I would be stuck with the auxiliary assumption $Az \rightarrow Rzz$, which I still have to use according to the deduction theorem.

I'm looking for some better suggestions!

EDIT -- THE FULL DEDUCTION

$\Sigma = \{\forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay)\}$

1 $\Sigma \vdash \forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay)$ assumption
2 $\vdash \forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay) \rightarrow \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay)$ Axiom schema 3
3 $\Sigma \vdash \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay)$ MP, 1, 2
4 $\vdash \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay) \rightarrow (Az \rightarrow Rzz) \rightarrow \neg Az$ Axiom schema 3
5 $\Sigma \vdash (Az \rightarrow Rzz) \rightarrow \neg Az$ MP, 3, 4
6 $\vdash Rzz \rightarrow (Az \rightarrow Rzz)$ axiom a
7 $Rzz \vdash Rzz$ assumption
8 $\Sigma, Rzz \vdash Az \rightarrow Rzz$ MP, 6, 7
9 $\Sigma, Rzz \vdash \neg Az$ MP, 5, 9
10 $\Sigma \vdash Rzz \rightarrow \neg Az$ deduction theorem, 9
11 $\Sigma \vdash \forall x (Rxx \rightarrow \neg Ax)$ Universal generalisation

The hardest part is step 6 and 7. At least, I always fall for it. I just cannot fathom coming up with some "random" formula derived from axiom a, and, even worse, taking the antecedent of that axiom a derived formula and use it as an auxiliary assumption (like step 7 did)...

Answer 1

We need :

$(\varphi \rightarrow \psi) \rightarrow \lnot \varphi \vdash (\psi \rightarrow \lnot \varphi)$.

Proof :

(1) $(\varphi \rightarrow \psi) \rightarrow \lnot \varphi$ --- assumed

(2) $\psi \rightarrow (\varphi \rightarrow \psi)$ --- Ax.a

(3) $\psi$ --- assumed

(4) $\varphi \rightarrow \psi$ --- from (2) and (3) by modus ponens

(5) $\lnot \varphi$ --- from (1) and (4) by modus ponens

(6) $\psi \rightarrow \lnot \varphi$ --- from (3) and (5) by Deduction Theorem.

Now you can restart from your :

5 $Σ \vdash (Az→Rzz)→¬Az$

to derive :

6 $Σ \vdash (Rzz→¬Az)$.