Proof of Powers with a Variable Base: a Predicative Formula and the Map (x, m) ↦ $x^m$

Proof of (i). The formula. Take the parameters $X$, $\cdot$, $\mathbb{N}$, and the order $\le$ and the addition $+$ of $\mathbb{N}_{0}$ to be the class variables $X$, $F$, $Y$, $R$ and $P$ of Iterated Operations Are Given by a Predicative Formula (i), with these values, and let $\mathrm{it}(z,m,a)$ be the predicative formula of that clause, with $z$, $m$ and $a$ for its $w$, $n$ and $a$ (a renaming as in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i)), $a$ being a set variable other than $x$, $m$, $z$ and the parameters. Let $q$ and $k$ be further distinct set variables of this kind, not occurring in $\mathrm{it}$. Let $\chi(x,a)$ be the formula $\forall q\,(q\in a\Leftrightarrow\exists k\,(k\in\mathbb{N}_{0}\wedge q=(k,x)))$, with $q=(k,x)$ the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii), and let $\pi(x,m,z)$ be the formula

$$x\in X\wedge m\in\mathbb{N}_{0}\wedge\Bigl((m=0\wedge z=e)\vee\bigl(m\in\mathbb{N}\wedge\exists a\,(\chi(x,a)\wedge\mathrm{it}(z,m,a))\bigr)\Bigr).$$

Its free variables are among $x$, $m$, $z$ and the parameters.

Predicativity. $\mathrm{it}$ is predicative by Iterated Operations Are Given by a Predicative Formula (i), and $q=(k,x)$ by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii); $\pi$ is built from these and from memberships and equations by connectives and by quantifiers over the set variables $a$, $q$ and $k$. The subformulas $\mathrm{it}$ and $q=(k,x)$, being predicative, contain no quantifier over a class variable, so no quantifier of $\pi$ is applied to a class variable, and $\pi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Meaning. Let $x$, $m$ and $z$ be sets. If $x\notin X$ or $m\notin\mathbb{N}_{0}$, both $\pi(x,m,z)$ and the condition fail. Let $x\in X$ and $m\in\mathbb{N}_{0}$. As $\mathbb{N}=\mathbb{N}_{0}\setminus\{0\}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)), exactly one of $m=0$ and $m\in\mathbb{N}$ holds.

If $m=0$, then $\pi(x,m,z)$ holds if and only if $z=e$; and $x^{0}=e$ by Powers with Exponents in the Natural Numbers with Zero (ii), $e$ being the neutral element of $\cdot$. So $\pi(x,m,z)$ holds if and only if $z=x^{m}$.

Let $m\in\mathbb{N}$. Let $c_{x}:\mathbb{N}_{0}\to X$ be the map with $c_{x}(k)=x$ for every $k\in\mathbb{N}_{0}$ (Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (i)). It is a set, being an element of $X^{\mathbb{N}_{0}}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $X$ and $\mathbb{N}_{0}$ being sets by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii); Classes, Membership, Sets and Proper Classes (i)), so it can be the value of the set variable $a$. For every set $q$: if $q\in c_{x}$, then $q=(k,v)$ for sets $k$ and $v$, $c_{x}$ being a relation (Functions, Values of a Function, and Functions from One Class to Another (iii)), with $k\in\mathbb{N}_{0}$ (Domains and Restrictions of Maps (i)) and $v=c_{x}(k)=x$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i)); and $(k,x)=(k,c_{x}(k))\in c_{x}$ for every $k\in\mathbb{N}_{0}$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii)). With Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii), $\chi(x,c_{x})$ holds, and a set $a$ satisfies $\chi(x,a)$ if and only if $a$ and $c_{x}$ have the same elements, that is, $a=c_{x}$. So $\exists a\,(\chi(x,a)\wedge\mathrm{it}(z,m,a))$ holds if and only if $\mathrm{it}(z,m,c_{x})$. The map $c_{x}$ is a map from the set $\mathbb{N}_{0}$, which contains $[m]$ (The Segments [n]: Each Is a Set, and 1 Lies in [n] for n ∈ ℕ (i)), to $X$; so by Iterated Operations Are Given by a Predicative Formula (i), $\mathrm{it}(z,m,c_{x})$ holds if and only if $z=\prod_{k=1}^{m}(c_{x})_{k}$, which by Iterated Operations: Finite Sums and Finite Products (ii) and Iterated Operations: Finite Sums and Finite Products (iii) is the iterated product of the restriction $c_{x}|_{[m]}$. Let $h:[m]\to X$ be the map $k\mapsto x$ on $[m]$ (Sets and Maps: Ordinary Notation (v)). Then $c_{x}|_{[m]}=[m]\times\{x\}=h$ by extensionality, as the elements of each of the three are exactly the pairs $(k,x)$ with $k\in[m]$. For $[m]\times\{x\}$ this holds by The Cartesian Product of Two Classes (i), the only element of the singleton $\{x\}$ being $x$ (The Empty Set, the Unordered Pair and the Singleton (iii)). For $c_{x}|_{[m]}$: a set $q$ lies in it if and only if $q\in c_{x}$ and $q=(u,v)$ for sets $u\in[m]$ and $v$ (The Restriction of a Function or Relation to a Class (i)); by the elements of $c_{x}$ found above, $[m]\subseteq\mathbb{N}_{0}$ and The Characteristic Property of Ordered Pairs and Nested Tuples of Sets (i), this holds if and only if $q=(k,x)$ for some $k\in[m]$. For $h$ it holds as for $c_{x}$ above, with $[m]$ for $\mathbb{N}_{0}$ and $h(k)=x$. So the iterated product of $c_{x}|_{[m]}$ is that of $h$, which is $\prod_{k=1}^{m}x$ by Iterated Operations: Finite Sums and Finite Products (i) and Iterated Operations: Finite Sums and Finite Products (iii), and this is $x^{m}$ by Powers with Exponents in the Natural Numbers with Zero (i). So $\pi(x,m,z)$ holds if and only if $z=x^{m}$.

Hence, under every assignment, $\pi(x,m,z)$ holds if and only if $x\in X$, $m\in\mathbb{N}_{0}$ and $z=x^{m}$: $\pi$ expresses this condition, as in Conditions Expressed by a Predicative Formula, and Guards (ii), with $x$, $m$ and $z$ for $x_{1}$, $x_{2}$ and $x_{3}$.

Proof of (ii). Let $\pi$ be the formula of the proof of (i). By (i), for all $x\in X$ and $m\in\mathbb{N}_{0}$, exactly one set $z$ satisfies $\pi(x,m,z)$, namely $x^{m}$. So $x^{m}$ is the defined set symbol with arguments $x$ and $m$ given by the predicative $\pi$, used properly where $x\in X$ and $m\in\mathbb{N}_{0}$.

For $x\in X$ and $m\in\mathbb{N}_{0}$, $x^{m}\in X$: for $m=0$, $x^{0}=e\in X$ (Associative and Commutative Binary Operations, and Neutral Elements (iii)); for $m\in\mathbb{N}$, $x^{m}=\prod_{k=1}^{m}x$ (Powers with Exponents in the Natural Numbers with Zero (i)), the iterated product of the map $k\mapsto x$ on $[m]$, which lies in $X$ by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set (i). $X$ and $\mathbb{N}_{0}$ are sets (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)). Hence Maps and Relations Given by Formulas (ii), applied to the sets $X$ (for $b$ and $c$) and $\mathbb{N}_{0}$ (for $d$) and the expression $t(v,w)=v^{w}$, gives exactly one map $p:X\times\mathbb{N}_{0}\to X$ with $p((x,m))=x^{m}$, that is, $p(x,m)=x^{m}$, for all $x\in X$ and $m\in\mathbb{N}_{0}$.