What is the negation of $\exists \lim\limits_{x \to a} f(x) \neq f(a)$, in precise FOL terms? Here is a quote from Spivak's Calculus:

If $\lim\limits_{x \to a} f(x)$ exists and is $\neq f(a)$, then $f$ is
said to have a removable discontinuity.

It appeared in a problem, not in the main text. It seems to be a definition. I believe it can also be written as a biconditional:
$$\exists \lim\limits_{x \to a} f(x) \neq f(a) \iff\ f \text{ has a removable discontinuity at } a\tag{1}$$
In another problem, we are asked to prove that a particular function never has a removable discontinuity.
My proof assumed the antecedent $\exists \lim\limits_{x \to a} f(x) \neq f(a)$, and used a proof by cases to show that a contradiction is obtained in all cases. Thus, I concluded that the negation of the antecedent is true, and hence that the negation of the consequent is true.
In other words, I concluded that:
$$\lnot (\exists \lim\limits_{x \to a} f(x) \neq f(a))\tag{2}$$
Therefore
$$\lnot (f \text{ has a removable discontinuity at } a)\tag{3}$$
Negating the entire antecedent is good enough for me to conclude that "for all $a$ f never has a removable discontinuity at $a$".
However, my question is about what exactly the negated antecedent is in terms of first-order logic. What is $(2)$, in very precise terms, ie in a way that is correct in a formal first-order logic sense?
The antecedent of $(1)$ itself doesn't seem precise. Should it be
$$(\exists \lim\limits_{x \to a} f(x)) \land (\lim\limits_{x \to a} f(x) \neq f(a))$$
But then when we negate this we get
$$(\nexists \lim\limits_{x \to a} f(x)) \lor (\lim\limits_{x \to a} f(x) = f(a))$$
Seems like the two conjuncts are linked in a way that makes the disjunction feel funny.
 A: The negation of $f$ having a removable discontinuity at $a$ is that either $f$ does not have a limit at $a$ or $f$ is continuous at $a$. The so-called "link" you speak of is that these conditions are mutually exclusive.
A: *

*$$∃y{,}l{\in}\mathbb R \;\Big(y=f(a)\;∧\;l=\lim\limits_{x \to a}
    f(x) \;∧\; y\neq l\Big)\\ \iff\\ f \text{ has a removable
    discontinuity at } a.$$

*$$∀a{,}y{,}l{\in}\mathbb R \;\Big(y\ne f(a) \;∨\; l\ne\lim\limits_{x
    \to a} f(x) \;∨\; f(a)= \lim\limits_{x \to a} f(x)\Big)\\ \iff\\ f
    \text{ has no removable discontinuity}\\ \iff$$ wherever $f$ is
defined, it is either continuous or non-removably discontinuous.

A: The negation is simply the following perfectly good English sentence: either the limit of $f$ at $a$ does not exist or it does exist but is not equal to $f(a)$. You could condense this as: $\lim_{x\to a} f(x)$ does not exist or $\lim_{x\to a} f(x)=f(a)$. This is the most easily comprehensible way of negating the sentence. No sequence of symbols is going to beat this.
But very well, your question seems to be: how do we formalize this as a formula of first-order logic? The difficulty that you encounter in your attempts stems from the fact that the claim "the limit $\lim_{x\to a} f(x)$ exists" seems like an existential quantification in first-order logic. The problem is that it isn't. First-order logic does not define $\exists$ as a meaningful syntactic unit at all. It only defines $\exists x$, where $x$ is a variable.
Now it seems like we could write something like: $\exists y ~ \lim_{x\to a} f(x) = y$. The problem with this is that standard first-order logic assumes that every term has a denotation. So, in particular, every term that you wish to interpret in the structure of real numbers must have a value which is a real number.
We see immediately that $\lim_{x\to a} f(x)$ cannot, in general, be a proper term of first-order logic. It does not always denote a real number. The proper way to formalize it is therefore to understand that notation like $\lim_{x\to a} f(x) = y$ is merely an informal manner of speaking.
One would properly formalize this in first-order logic as something like $\mathrm{LimitOfFunctionExistsAndIsEqualTo}(f,a,y)$, which would then be expanded into the actual epsilon-delta definition of a limit. So you could say that the negation is simply:
$\mathrm{LimitOfFunctionExistsAndIsEqualTo}(f,a,f(a)) \vee \neg \exists y \, \mathrm{LimitOfFunctionExistsAndIsEqualTo}(f,a,y)$
This does not seem like an improvement on the informal but perfectly precise English sentence.
(I am papering over one additional difficulty here, which is that I am using one letter for a function variable and another letter for a numeric variable. Again, this is not something one does in standard single-sorted first-order logic.)
