On notation, at first I just write $\exists^{!\infty}$, later I changed to $\exists^\infty$, which one should I use $?$
And I'm thinking what does this really mean in first-order-logic$\dots$
My attempts (first formalize at least, at most, exact)
$\text{Let n $\in\mathbb{N}$, then }\exists^{\ge n}x,p(x) \text{ if and only if :}$ $$\exists x_1\dots x_n \text{ s.t.}\underbrace{(p(x_1)\wedge\dots\wedge p(x_n))}_{\text{$x_1\dots x_n$ satisfy $p$}} \wedge\underbrace{(x_1\neq x_2\land\dots\land x_1\neq x_n)\wedge\dots\wedge(x_{n-1}\neq x_n)}_{\text{$x_1\dots x_n$ are distinct}}$$ $$\Leftrightarrow\underset{i=1}{\overset{n}{\exists}} x_i,(\bigwedge_{i=1}^np(x_i))\wedge(\bigwedge_{i=1}^{n-1}(\bigwedge_{j=i+1}^nx_i\neq x_j))$$
$\exists^{\le n}x,p(x) \text{ if and only if :}$ $$\exists^{<n+1}x,p(x)$$ $$\Leftrightarrow\neg(\exists^{\ge n+1}x,p(x))$$ $$\Leftrightarrow \underset{i=1}{\overset{n+1}{\forall}}x_i,(\bigvee_{i=1}^{n+1}\neg p(x_i))\vee(\bigvee_{i=1}^n(\bigvee_{j=i+1}^{n+1}x_i=x_j))$$
$\exists^{!n}x,p(x) \text{ if and only if :}$ $$\exists^{\ge n}x,p(x)\wedge\exists^{\le n}x,p(x)$$ $$\Leftrightarrow\exists^{\ge n}x,p(x)\wedge\neg(\exists^{\ge n+1}x,p(x))$$ $$\Leftrightarrow \underset{i=1}{\overset{n}{\exists}}x_i\forall x_{n+1}(p(x_{n+1})\leftrightarrow(\bigvee_{i=1}^nx_i=x_{n+1}))\wedge\bigwedge_{i=1}^{n-1}(\bigwedge_{j=i+1}^nx_i\neq x_j)$$
The idea is first we define at least $n$, then we notice that at most $n$ is just not (at least $n+1$), also notice exactly $n$ is just at least $n$ and at most $n$.
Then, to express exists infinitely many we can write
$\exists^{\infty}x,p(x)$ if and only if: $$\forall n\in\mathbb{N},\exists^{\ge n}x,p(x)$$
$$\Leftrightarrow \forall n\in\mathbb{N},\underset{i=1}{\overset{n}{\exists}} x_i,(\bigwedge_{i=1}^np(x_i))\wedge(\bigwedge_{i=1}^{n-1}(\bigwedge_{j=i+1}^nx_i\neq x_j))$$
And by taking negation, exists finitely many can be expressed as
$\exists^{<\infty} x, p(x)$ if and only if:
$$\exists n\in\mathbb{N},s.t.\exists^{\le n-1},p(x)$$ $$\Leftrightarrow \exists n\in\mathbb{N},s.t.\underset{i=1}{\overset{n}{\forall}}x_i,(\bigvee_{i=1}^{n} \neg p(x_i))\vee(\bigvee_{i=1}^{n-1}(\bigvee_{j=i+1}^{n}x_i=x_j))$$
Is this correct, any suggestion would be appreciated.
The standard notation in logic would be $\exists^\infty$.
The exclamation mark ! is used to indicate uniqueness, $\exists^{!n} x\,\phi(x)$ being "there are exactly $n$ distinct elements $x$ such that $\phi(x)$". So, the standard reading of $\exists^{!\infty}x\,\phi(x)$ would be "there are exactly infinitely many $x$ such that..." which is awkward, as it is not very exact to simply say "infinitely many", since there are many options here. And if you are in a setting where the universe of discourse is countably infinite, for instance, then the "exactly" part is superfluous anyway.
You are correct that $\exists^{\infty}x\,\phi(x)$ is the same as $\forall n\,\exists^{\ge n}x\,\phi(x)$. This is the case regardless of whether you are in a situation where the axiom of choice holds. I mention this because using choice, $\exists^{\infty}x\,\phi(x)$ is equivalent to $Q_{\aleph_0}x\,\phi(x)$, where $\aleph_0=|\mathbb N|$ and, for a cardinal $\kappa$, $Q_\kappa x\,\phi(x)$ means that there are at least $\kappa$ distinct values of $x$ such that ... (The $Q_\kappa$ are called cardinality quantifiers in the literature.) However, if choice fails, a set may be infinite without containing a countably infinite subset.
(And just to avoid confusion, let me add the remark mentioned in comments: Although each $\exists^{\ge n}$ is first-order definable as shown in the question, $\exists^\infty$ is a genuinely new quantifier, meaning that it is not first-order definable by a formula. Otherwise, its negation ("there are only finitely many") would also be first-order definable, and an easy compactness argument gives us a contradiction: the theory $$\{\lnot\exists^\infty x\,(x=x)\land\exists^{\ge n}x\,(x=x)\mid n\in\mathbb N\}$$ is inconsistent but any finite subset is consistent.)