The usual proof that the ordinal notations for ordinals below $\varepsilon_0$ is well-ordered takes place in set theory and uses the fact that actual ordinals (i.e., not notations) are well-ordered.
The proof relies on Cantor Normal Form: that every ordinal $\alpha$ can be written in a unique way in the form $$\alpha = \omega^{\beta_1}n_1 + \omega^{\beta_2}n_2 + \cdots + \omega^{\beta_k}n_k$$ where $\beta_1 \gt \beta_2 \gt \cdots \gt \beta_k$ and $1 \leq n_1,n_2,\ldots, n_k \lt \omega$.
By induction on $\alpha \lt \varepsilon_0$, show that $\alpha$ has a unique ordinal notation. To do this, note that f $\alpha \lt \varepsilon_0$ then we must have $\alpha \gt \beta_1 \gt \beta_2 \gt \cdots \gt \beta_k$ and so each exponent $\beta_i$ has been shown to have a unique notation.
The result of this process is an order-preserving function from the ordinal $\varepsilon_0$ to your set of notations which is the inverse of the evaluation map that goes the other way around. This isomorphism shows that your set of notations is well-ordered.
If you're concerned about using ZFC, note that this proof works in much weaker systems of set theory. If you're still concerned, you can actually work in subsystems of second-order arithmetic.
The trick to make things work in second-order arithmetic is explained in the excellent paper:
Alberto Marcone and Antonio Montalbán, The Veblen functions for computability theorists, J. Symbolic Logic 76 (2011), no. 2, 575--602; arXiv:0910.5442.
What you need is contained in Theorem 3.1:
If $\mathcal{X}$ is a $Z$-computable linear ordering, and $\omega^{\mathcal{X}}$ has a $Z$-computable
descending sequence, then $Z'$ can compute a descending sequence in $\mathcal{X}$.
Since $\omega$ is well-ordered, we can use this to show even in $\mathsf{ACA}_0$ that $\omega^\omega$ is well-ordered, that $\omega^{\omega^\omega}$ is well-ordered, etc. Since $\mathsf{ACA}_0$ has limited induction, this does not prove that $\varepsilon_0$ is well-ordered in $\mathsf{ACA}_0$. (Indeed, the proof-theoretic ordinal of $\mathsf{ACA}_0$ is $\varepsilon_0$!) However, this does easily show that $\varepsilon_0$ is well-ordered in the standard model of second-order arithmetic, which appears to be enough for your purposes. (If I misunderstood your purposes, keep reading to Theorem 3.4 which shows that $\varepsilon_0$ is provably well-ordered in $\mathsf{ACA}_0^+$.)
