**Ended Competition:** What is the shortest proof of $\exists x \forall y (D(x) \to D(y)) $?

Well, here's my solution even though I've used 4 'unallowed' rules.

1. $\neg\exists x\forall y(Dx\implies Dy)\quad$ assumption for $\neg$ introduction
2. $\forall x\neg\forall y(Dx\implies Dy)\quad$ DeMorgan's for quantifiers
3. $\forall x\exists y \neg(Dx\implies Dy)\quad$ DeMorgan's for quantifiers
4. $\forall x\exists y\neg(\neg Dx\vee Dy)\quad$ Conditional exchange
5. $\forall x\exists y(\neg\neg Dx\wedge \neg Dy)\quad$ DeMorgan's
6. $\forall x \exists y(Dx\wedge\neg Dy)\quad$ Double negation
7. $\exists y(Da\wedge\neg Dy)\quad$ Universal instantiation
8. $Da\wedge \neg Db\quad$ Existential instantiation (flag $b$)
9. $\neg Db\quad$ Simplification
10. $\exists y(Db\wedge \neg Dy)\quad$ Universal instantiation
11. $Db\wedge \neg Dc\quad$ Existential instantiation (flag $c$)
12. $Db\quad$ Simplification
13. $\bot\quad$ Contradiction 9, 12
14. $\neg\neg\exists x\forall y(Dx\implies Dy)\quad$ Proof by contradiction 1-13
15. $\exists x\forall y(Dx\implies Dy)\quad$ Double negation

I guess there are 16 lines in all if we include the empty premise line. I do have a couple comments though.

First, I highly doubt this proof can be attained by the last applied rule being Existential Generalization. This statement is a logical truth precisely because we can change our $x$ depending on whether the domain has or has not a member such that $Dx$ holds. If $D$ holds for all members of the domain, any choice of $x$ will make the statement true. If $D$ does not hold for some member of the domain, choosing that as our $x$ will make the statement true. Saying that we can reach the conclusion by one final use of E.G. means that the member $b$ which appears in the precedent somehow handled both cases while the only thing we are supposed to know about $b$ is that it is a member of the domain. We still don't know anything of the domain.

With that said, after I got a copy of your book and read the rules, it appears the only way we can get to the conclusion is by an application of double negation. And the only way to get there is a proof by contradiction. Thus I believe your lines 1, 2, 19, 20, and 21 belong to the minimal solution. So far, I haven't found anything simpler for the middle.

Although outside the scope of what is asked, it is perhaps amusing to note that a proof in a tableau system is markedly shorter, and writes itself (without even having to split the tree and consider cases):

$$\neg\exists x\forall y(Dx\implies Dy)$$ $$\forall x\neg\forall y(Dx\implies Dy)$$ $$\neg\forall y(Da\implies Dy)$$ $$\exists y\neg(Da\implies Dy)$$ $$\neg(Da\implies Db)$$ $$\neg Db$$ $$\neg\forall y(Db\implies Dy)$$ $$\exists y\neg(Db\implies Dy)$$ $$\neg(Db\implies Dc)$$ $$Db$$ $$\bigstar$$

This isn't quite an answer, since it's about the Drinker's paradox, and not the slightly different version here, but it may help for developing a shorter proof of the variant here. The line count might not be acceptable though, because it uses Taut Con, but only to get $A$ and $\lnot B$ from $\lnot (A \to B)$, not for any quantifier exchange or anything like that. The accepted answer uses some DeMorgan's with quantifers though, so I think this might be within bounds.

Using the Fitch software that's distributed with the LPL book, you can get the Drinker's Paradox down to 14 lines, because of the way that $\forall$-introduction is allowed to cite any intermediate result in the proof, not just the last one.

Note: The image says "bird" because when I first heard this, it was phrased as "there's something such that if it's a bird, then everything is a bird." I made this proof back in 2009 and don't have access to the original files anymore, so sorry about the image quality.

Maybe this can help shorten a proof of the variant.