How do we formalize in $\mathbf{PA}$ that for some arithmetical formula $\varphi(x)$ there exists an $m$ that expresses the number of $n \leq \ell$ such that $\varphi(n)$, and from this obtain
$\mathbf{PA} \vdash \exists \text{ different } n_1, \dots, n_m \in \{0, \dots, \ell\} \bigwedge^m_{j=1} \varphi(n_j)$;
$\mathbf{PA} \vdash \bigwedge^m_{j=1} \varphi(\overline{k_j}) \to \neg\varphi(\bar{x})$ where all $k_j \leq \ell$ are different and $x \in \{0, \dots, \ell\} \setminus \{k_1, \dots, k_m\}$ is arbitrary.
I'm mainly looking for intuition on how such formalization works if you were to be forced to write them out in some detail.
Since you're just asking for intuition I won't write everything out explicitly, but the idea is by applying the law of the excluded middle you can show exactly one sentence of the form $$(\neg)\phi(0)\land(\neg)\phi(1)\land...\land(\neg)\phi(\ell)$$ must be true (that is, since each $\phi(n)$ is true or false the only way of making this sentence true is negating exactly the false sentences). You can then partition these sentences by the number of $\phi$'s that are not negated in this expression. The class of the partition our unique true sentence lands in is our $m$, and (2) follows from the the fact that this was the only sentence of the described form that was true.