Why is $0^\sharp$ not definable in $ZFC$?

The phrase "$0^\sharp$ exists" refers not merely to the existence of that set, but rather also to the assertion that this collection of formulas has the property of being the type of order-indiscernibles in $L$. So one should take the phrase "$0^\sharp$ exists" as asserting not just that that set exists, but also that it has certain properties that make $0^\sharp$ what it is.

Of course, one can always define in ZFC the type of the cardinals $\aleph_n$ in $L$, just as you wrote it down. And there is no problem with defining that set. But in some ZFC models, that set won't give you any power, the reason you would want to care about $0^\sharp$.

For this reason, I find the "$0^\sharp$ exists" terminology to be a little unfortunate. What the phrase is meant to evoke is that there is a combinatorial object with a certain property that we can describe, which gives us the theory of order-indiscernibles for $L$. When it does exist, it happens to be equal to the set you defined, but that set doesn't always have the desired combinatorial property.

The classical definition of $0^\sharp$ is as (the set of Gödel numbers of) a theory, namely, the unique Ehrenfeucht-Mostowski blueprint satisfying certain properties (coding indiscernibility). This is a perfectly good definition formalizable in $\mathsf{ZFC}$, but $\mathsf{ZFC}$ or even mild extensions of $\mathsf{ZFC}$ are not enough to prove that there are objects that satisfy it. In $L$ there is no EM blueprint with the required properties.

It happens that if it exists, then $0^\sharp$ indeed admits the simple description given in line 4 of your question, but (unlike $0^\sharp$) the set in line 4 always exists (that is, $\mathsf{ZFC}$ proves its existence, pretty much along the lines of the sketch you suggest), so it is not appropriate to define $0^\sharp$ that way (for instance, that set is not forcing invariant in general).

As you mentioned, there are several equivalent definitions of $0^\sharp$. Some of them are readily formalizable in $\mathsf{ZFC}$, some are not. For example, we cannot talk of a proper class of $L$-indiscernibles in $\mathsf{ZFC}$ alone, but $0^\sharp$ could be defined as such a class.

The modern definition of $0^\sharp$ introduces it not as a theory but rather as a certain mouse, a model of the form $(L_\alpha,U)$ for certain $\alpha$, where $U$ is an (external) $L$-$\kappa$-ultrafilter for some $\kappa$ definable in terms of $\alpha$, with the requirement that the iterates of $L_\alpha$ by $U$ are all well-founded (and some additional technical requirements related to the minimality of this model). This is more in tune with the current approach to inner model theory. Again, this definition is formalizable in $\mathsf{ZFC}$ in a straightforward fashion, but the existence of such a mouse cannot be established in $\mathsf{ZFC}$ alone.