Ordinal Exponentiation Levy Hierarchy It is a standard exercise (see Jech's "Set Theory" Exercise 13.8) to prove that ordinal addition and multiplication are $\Delta_1$ expressible functions.  The proof for addition comes from noting that $\alpha+\beta$ is order isomorphic to the disjoint union $(\{1\}\times \alpha)\cup (\{2\}\times \beta)$ under the lexicographical order (and everything after the "order isomorphic" part is all $\Delta_0$ expressible).  Similarly $\alpha\cdot \beta$ is order isomorphic to the direct product $\beta\times \alpha$ under the lexicographical order.
It was surprised to see that ordinal exponentiation was not listed in the exercise.  After a serious google search, the only reference I could find was a wiki article that claimed ordinal exponentiation was indeed $\Delta_1$.  I couldn't make the same argument work here, since the corresponding order structure for $\alpha^\beta$ is the set $\{f:\beta\to \alpha\,|\, f\text{ has finite support}\}$ and I couldn't find an easy way to express this set in a $\Sigma_1$ way.
Is ordinal exponentiation $\Sigma_1$?  If so, how does the proof go?  (Hopefully I didn't miss an easy argument!)
(This also raised the question in my mind of whether or not, given $X$, the set of finite subsets of $X$ is $\Sigma_1$.  I'd like to know the answer to that as well.)

Added: If I didn't make any mistakes, ordinal exponentiation is $\Delta_1$ if and only if that finite support set above is $\Delta_1$ definable.  Thus, in principle, there should be an easy way to get a $\Sigma_1$ definition of that set.  This seems surprising to me.
 A: First, I claim that one can express in $\Delta_1$ form the following property of $\alpha,\gamma, g$, which I'll abbreviate as $P(\alpha,\gamma,g)$: $\alpha$ and $\gamma$ are ordinals, $g$ is a function with domain $\gamma$, and, for each $\beta<\gamma$, $g(\beta)$ is the set of finitely supported functions $f:\beta\to\alpha$. Being an ordinal and being a function with a specified domain are easily $\Delta_1$, so the problem is to specify the values $g(\beta)$.  But this can be done by saying that $g(0)=\{\varnothing\}$, that the elements of $g(\beta+1)$ are exactly the things of the form $f\cup\{\langle\beta,\xi\rangle\}$ with $f\in g(\beta)$ and $\xi<\alpha$ (for each $\beta+1<\gamma$), and that, for all limit ordinals $\lambda<\gamma$, the elements of $g(\lambda)$ are exactly the things of the form $f\cup((\lambda-\beta)\times\{0\})$ with $\beta<\lambda$ and $f\in g(\beta)$.
Once we have this $\Delta_1$ definition of $P$, we can express "$x$ is the set of finitely supported functions $\beta\to\alpha$" by saying "there exists $g$ such that $P(\alpha,\beta+1,g)$ and $g(\beta=x)$."  Except for "there exists $g$", everything here is $\Delta_1$, so the whole statement is $\Sigma_1$.
The same idea, for converting a recursive definition to an explicit definition, can be used to support my earlier comment about using the recursive definitions of addition, multiplication, and exponentiation to show that these are $\Delta_1$-definable.  One says, for example, that $\alpha^\beta=\theta$ iff there is a function $g$ with domain $\beta+1$ satisfying the inductive clauses for the definition of exponentiation and $g(\beta)=\theta$. That's a $\Sigma_1$ definition and, since exponentiation is provably total, $\Delta_1$-definability follows.  (As far as I know, the idea of converting recursive definitions to explicit ones goes back to Dedekind.)
