The constraint $a,x>0$ gives a nice start. Then $a$ and $a$ can be interchanged without change in the function under examination.
So at the border of the range of consideration, there is:

The only thing that is now to show that the function is strictly monotonically increasing.
The first derivative is
$a x^{a-1}+a^x ln(x)$
Again the symmetry of exchange of 2both variables is nice. Both derivatives are the same in structure and composition.
The graph shows that this is valid for $a,x>1$ for sure.
[
]
The is a problem with the border. The function is not defined for $a,x$ approaching $0$ caused by the logarithms while it exists at a different value.
We know the behavior of the potential and logarithmic function and have proven the hypothesis for $a,x>1$. The logarithm is negative for $a,x<1$ there is the problem.
That is a graph of it:

Look at this at the line where $a==x$!

This reduces the problem from 2D to 1D exemplarily.

There is crossing with the x-axis and the function is on that path again rising! It has a minimum value larger than 1.
That point is $\frac{1}{e},0$ the function has the value $2\frac{1}{e}^{-\frac{1}{e}}=e^{-\frac{1}{e}} $.
Again we have a different value at $(0,0)$ at this time $2$.
So this proves both the function is greater than $1$ in $a,x$>0$ and there are no unique values of the function for $(0,0)$! This value depends on the path on which $(0,0)$ is approached. The value in $(0,0)$ is a continuous completion of each path.
We thereby found that the function is dropping between $(0,0)$ and a point between $0<b<1$ which too varies on the path we use but is unique on that.
That can be formulated in find the minimum of $x^a+a^x$ in $(0,1)x(0,1)$.
The value named is the global minimum of the function on the selected path. On the curve of minima, it is a maximum. Since we know the value on the axes and that the curve is steady more than that steady differentiable infinitely often.
With that knowledge it is proven that the function is for $x,a>0$ greater than $1$ but in $(0,0)$ undefined and multivalued dependent on the path of approach.
This is not the complete formal proof but a rich informal proof with plenty of the elements of the formal proof. The deviation from the formal proves a due to less complexity in formulations. The curiosity of the problem is presented several times. The formal proof uses methods from real calculus. This problem may deserve complex calculus because of the multi-valueness at the origin.
The informal elements are the main advantages of the proof such as symmetry that need a more detailed write down for higher expectation of mathematical formal correctness, strictness.
This is one of the wonders of Mathematics restricted to the $Reals$, $\mathbb R$ and the potency function together with the logarithm in the context of inverse functions calculation.