Proof of Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set

Each result cited is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Formulas. The formulas below are formulas of class theory as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols, written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols and read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading. Elements of $\mathbb{N}_{0}$ are assigned to set variables and read as sets only in that sense; a variable to which a number is assigned occurs only to the left of $\in$, as a component of an ordered pair, or as an argument of a formula $\mathrm{it}$ below. The data fixed in a clause are assigned to distinct variables, its parameters, named where they are used; all other variables are set variables, distinct from the parameters and from one another. Each formula $\theta$ below is built from parts that are predicative, by the connectives and by quantifiers over set variables; its parts apply no quantifier to a class variable and $\theta$ adds none, so $\theta$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure.

Maps from formulas. We use the following form (M) of Maps and Relations Given by Formulas §map. Let $U$ and $V$ be sets, let a set $c(u)\in V$ be given for each $u\in U$, and let $\theta(w,u)$ be a predicative formula, with $w$ and $u$ distinct set variables and its parameters assigned, such that for every $u\in U$ and every set $w$, $\theta(w,u)$ holds if and only if $w=c(u)$. Then there is exactly one map $g:U\to V$ with $g(u)=c(u)$ for every $u\in U$. Indeed, for $u\in U$ exactly one set $w$ satisfies $\theta(w,u)$, namely $c(u)$; so the set $\tau(u)$ with $\theta(\tau(u),u)$ is a defined set symbol given by $\theta$, with argument $u$, used properly wherever the hypothesis $u\in U$ is in force, as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination with $\gamma(u)$ the formula $u\in U$, $U$ being assigned to a further parameter; and $\tau(u)=c(u)\in V$. By Maps and Relations Given by Formulas §map, applied to the expression $\tau(u)$, there is exactly one map $g:U\to V$ with $g(u)=\tau(u)=c(u)$ for every $u\in U$.

Values and restrictions. (V0) Values of a map lie in its codomain: for classes $D$ and $E$, a map $F:D\to E$ and a set $u\in D$, $F(u)\in E$ by Functions, Values of a Function, and Functions from One Class to Another §value and Functions, Values of a Function, and Functions from One Class to Another §map. Let $\ast$ be a binary operation on a set $X$, let $n\in\mathbb{N}$, and let $[n]$ be as in Intervals of Natural Numbers §segment. (V1) For a set $D$ with $[n]\subseteq D$ and a map $a:D\to X$, the restriction $a|_{[n]}$ is a map $[n]\to X$ with value $a(k)$ at each $k\in[n]$: by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction it is a function with domain $[n]\cap D=[n]$ and value $a(k)$, which lies in $X$ by (V0), at each $k\in[n]$; each element of its range is one of these values, by Functions, Values of a Function, and Functions from One Class to Another §value, so it is a map $[n]\to X$ by Functions, Values of a Function, and Functions from One Class to Another §map. (V2) For such $a$, $\mathop{\ast}\limits_{k=1}^{n}a_{k}$ is the iterated operation of $a|_{[n]}$ by Iterated Operations: Finite Sums and Finite Products §restriction, which by Iterated Operations: Finite Sums and Finite Products §iterated is a value of the map $s:[n]\to X$ of Iterating a Binary Operation along a Finite List §existence; so it lies in $X$ by (V0). If $D=[n]$, then $a|_{[n]}=a$ by (V1) and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, so the readings of Iterated Operations: Finite Sums and Finite Products §iterated and Iterated Operations: Finite Sums and Finite Products §restriction agree. (V3) If $t\in X$ and $a(k)=t$ for every $k\in[n]$, then $\mathop{\ast}\limits_{k=1}^{n}a_{k}$ is the iterated operation of the constant map $k\mapsto t$ on $[n]$ of Sets and Maps: Ordinary Notation §maps, that is $\mathop{\ast}\limits_{k=1}^{n}t$ in the notation of Iterated Operations: Finite Sums and Finite Products §iterated: that map and $a|_{[n]}$ are functions with domain $[n]$ and value $t$ at every $k\in[n]$, by (V1), so they are equal by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Finally, $[n]=\{k\in\mathbb{N}:k\le n\}\subseteq\mathbb{N}$ for every $n\in\mathbb{N}$, by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment.

The formula for iterated operations. Let $\ast$ be a binary operation on a set $X$. Assign $X$, $\ast$, $\mathbb{N}$, the order $\le$ of $\mathbb{N}_{0}$ and the addition $+$ of $\mathbb{N}_{0}$ to distinct class variables $X$, $F$, $Y$, $L$ and $P$, taken for the variables $X$, $F$, $Y$, $R$ and $P$ of Iterated Operations Are Given by a Predicative Formula §predicative. For any distinct set variables $w$, $n$ and $b$, that clause gives a predicative formula $\mathrm{it}(w,n,b)$, with free variables among $w$, $n$, $b$, $X$, $F$, $Y$, $L$ and $P$, such that for every $n\in\mathbb{N}$, every map $b$ from a set containing $[n]$ to $X$, and every set $w$, $\mathrm{it}(w,n,b)$ holds if and only if $w=\mathop{\ast}\limits_{k=1}^{n}b_{k}$.

Clause iterates. Let $\ast$, $X$ and $a:\mathbb{N}\to X$ be as in Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §iterates, with the parameters of $\mathrm{it}$ assigned as in the preceding paragraph and $a$ assigned to the set variable $a$. Let $\theta(w,n)$ be $\mathrm{it}(w,n,a)$, which is predicative. For $n\in\mathbb{N}$, $a$ is a map from $\mathbb{N}\supseteq[n]$ to $X$, so for every set $w$, $\theta(w,n)$ holds if and only if $w=\mathop{\ast}\limits_{k=1}^{n}a_{k}$, and this set lies in $X$ by (V2). By (M), with $\mathbb{N}$, $X$ and $c(n)=\mathop{\ast}\limits_{k=1}^{n}a_{k}$, there is exactly one map $s:\mathbb{N}\to X$ with $s(n)=\mathop{\ast}\limits_{k=1}^{n}a_{k}$ for every $n\in\mathbb{N}$.

Two cases. For a set $X$, an element $e\in X$ and a map $s:\mathbb{N}\to X$, assign $\mathbb{N}$ to the class variable $N$ and $e$ and $s$ to distinct set variables $e$ and $s$, and let $\theta_{e,s}(w,n)$ be

$$(\neg\,n\in N\wedge w=e)\vee(n\in N\wedge(n,w)\in s).$$

Its part $(n,w)\in s$ is predicative 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 §pair-membership, and its other parts are atomic, so $\theta_{e,s}$ is predicative. Let $n\in\mathbb{N}_{0}$ and let $w$ be a set. If $n\notin\mathbb{N}$, then $n=0$, as $\mathbb{N}=\mathbb{N}_{0}\setminus\{0\}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, and $\theta_{e,s}(w,n)$ holds if and only if $w=e$. If $n\in\mathbb{N}$, then $n\in\operatorname{dom}s$ by Functions, Values of a Function, and Functions from One Class to Another §map, and $\theta_{e,s}(w,n)$ holds if and only if $(n,w)\in s$, that is, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, if and only if $w=s(n)$. Hence, if $t(0)=e$ and $t(n)=s(n)$ for $n\in\mathbb{N}$, then for every $n\in\mathbb{N}_{0}$ and every set $w$, $\theta_{e,s}(w,n)$ holds if and only if $w=t(n)$, and $t(n)\in X$, by (V0) for $n\in\mathbb{N}$. By (M), with $\mathbb{N}_{0}$, $X$ and $c=t$, there is exactly one map $p:\mathbb{N}_{0}\to X$ with $p(n)=t(n)$ for every $n\in\mathbb{N}_{0}$.

Clause images. Let $R$ be as in Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §images; $+$ is a binary operation on $R$ by Commutative Rings §ring. Let $g:\mathbb{N}\to R$ be the constant map $k\mapsto1$ of Sets and Maps: Ordinary Notation §maps, and let $s:\mathbb{N}\to R$ be the map of the clause iterates for $+$ and $g$, so $s(n)=\sum_{k=1}^{n}g_{k}$ for $n\in\mathbb{N}$. For $n\in\mathbb{N}$, $g(k)=1$ for every $k\in[n]\subseteq\mathbb{N}$, so by (V3) $s(n)$ is the finite sum of the constant map $k\mapsto1$ on $[n]$, which is $n_{R}$ by The Image of a Natural Number in a Commutative Ring §image. Also $0_{R}=0$ by The Image of a Natural Number in a Commutative Ring §image, and $0\in R$. The paragraph on two cases, with $X=R$, $e=0$ and this $s$, gives exactly one map $\nu:\mathbb{N}_{0}\to R$ with $\nu(0)=0=0_{R}$ and $\nu(n)=s(n)=n_{R}$ for $n\in\mathbb{N}$; as every $n\in\mathbb{N}_{0}$ is $0$ or lies in $\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, these are exactly the maps with $\nu(n)=n_{R}$ for every $n\in\mathbb{N}_{0}$.

Clause powers. Let $\cdot$, $X$ and $x$ be as in Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §powers, and let $e$ be a neutral element of $\cdot$; by A Binary Operation Has at Most One Neutral Element §unique it is the only one, so $x^{0}=e$ by Powers with Exponents in the Natural Numbers with Zero §zero. Let $g:\mathbb{N}\to X$ be the constant map $k\mapsto x$ of Sets and Maps: Ordinary Notation §maps, and let $s:\mathbb{N}\to X$ be the map of the clause iterates for $\cdot$ and $g$, so $s(n)=\prod_{k=1}^{n}g_{k}$ for $n\in\mathbb{N}$. For $n\in\mathbb{N}$, $g(k)=x$ for every $k\in[n]\subseteq\mathbb{N}$, so by (V3) $s(n)=\prod_{k=1}^{n}x$, which is $x^{n}$ by Powers with Exponents in the Natural Numbers with Zero §power. The paragraph on two cases, with this $X$, $e$ and $s$, gives exactly one map $p:\mathbb{N}_{0}\to X$ with $p(0)=e=x^{0}$ and $p(n)=s(n)=x^{n}$ for $n\in\mathbb{N}$, and as in the clause images these are exactly the maps with $p(n)=x^{n}$ for every $n\in\mathbb{N}_{0}$.

Clause ring-powers. Let $R$ and $x$ be as in Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §ring-powers; $\cdot$ is a binary operation on $R$ by Commutative Rings §ring. For every $y\in R$, $y\cdot1=y$ and $1\cdot y=y\cdot1=y$ by Commutative Rings §ring, so $1$ is a neutral element of $\cdot$. Hence $x^{0}=1$ by Powers with Exponents in the Natural Numbers with Zero §zero and A Binary Operation Has at Most One Neutral Element §unique, and the clause powers, with $X=R$, gives exactly one map $p:\mathbb{N}_{0}\to R$ with $p(n)=x^{n}$ for every $n\in\mathbb{N}_{0}$.

Clause finite-operation. Let $\ast$, $X$, $A$, $B$ and $f:A\times B\to X$ be as in Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §finite-operation.

The maps $f_{x}$. Let $x\in A$. For $y\in B$, $(x,y)\in A\times B$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, which is the domain of $f$ by Functions, Values of a Function, and Functions from One Class to Another §map; so the expression $f((x,y))=f(x,y)$, built from the ordered pair and the value of $f$, is used properly, and $f(x,y)\in X$ by (V0). So the map $f_{x}:B\to X$, $y\mapsto f(x,y)$, of Sets and Maps: Ordinary Notation §maps is defined: it is the unique map $B\to X$ with $f_{x}(y)=f(x,y)$ for every $y\in B$, by Maps and Relations Given by Formulas §map.

The case $B=\emptyset$. Then $\ast$ has a neutral element $e\in X$. For $x\in A$ let $c(x)=\mathop{\ast}\limits_{y\in B}f_{x}(y)$; then $c(x)=e$ by Sums and Products over a Finite Set and over an Interval §empty, so $c(x)=e\in X$. With $e$ assigned to the set variable $e$, the atomic formula $w=e$ holds, for every $x\in A$ and every set $w$, if and only if $w=c(x)$. By (M), with $A$, $X$, the formula $\theta(w,x)$ given by $w=e$ and this $c$, there is exactly one map $h:A\to X$ with $h(x)=\mathop{\ast}\limits_{y\in B}f_{x}(y)$ for every $x\in A$.

The case $B\neq\emptyset$. Let $n=\#B$ as in The Number of Elements of a Finite Set §cardinality, and fix a bijection $\varphi$ from $[n]$ onto $B$, which exists by The Number of Elements of a Finite Set §cardinality; it is a map $\varphi:[n]\to B$ by Injective, Surjective and Bijective Functions between Classes §bijective. Then $n=\#B\in\mathbb{N}$: $n\in\mathbb{N}_{0}$, and $n\neq0$, since an element of $B$ is $\varphi(k)$ for some $k\in[n]$ by Injective, Surjective and Bijective Functions between Classes §surjective, while $[0]=\emptyset$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment; so $n\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets. Assign the parameters of $\mathrm{it}$ for $\ast$ as in the paragraph on the formula for iterated operations, and assign $n$, $[n]$, $\varphi$ and $f$ to distinct set variables $n$, $d$, $\varphi$ and $f$. With $\mu$ 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 §map, its variables $F$, $A$ and $B$ replaced by $b$, $d$ and $X$, let $\theta(w,x)$ be

$$\exists b\,\Bigl(\mu(b,d,X)\wedge\forall k\,\forall y\,\forall q\,\bigl(((k,y)\in\varphi\wedge((x,y),q)\in f)\Rightarrow(k,q)\in b\bigr)\wedge\mathrm{it}(w,n,b)\Bigr),$$

where $b$, $k$, $y$ and $q$ are set variables distinct from one another, from the parameters, from $w$ and $x$, and from the variables $p$, $u$, $u'$, $v$ and $v'$ of that clause. Its parts are predicative: $\mu(b,d,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 §map, $(k,y)\in\varphi$ and $(k,q)\in b$ 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 §pair-membership, $((x,y),q)\in f$ 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 §operation-membership, and $\mathrm{it}(w,n,b)$ by Iterated Operations Are Given by a Predicative Formula §predicative; so $\theta$ is predicative.

Fix $x\in A$. For $k\in[n]$, $\varphi(k)\in B$ by (V0), so the expression $f((x,\varphi(k)))=f(x,\varphi(k))$ is used properly and lies in $X$, as for the maps $f_{x}$; by Maps and Relations Given by Formulas §map there is exactly one map $a^{x}:[n]\to X$ with $a^{x}(k)=f(x,\varphi(k))=f_{x}(\varphi(k))$ for every $k\in[n]$. We show that, for every set $b$, the conjunction $\beta(b)$ of the first two parts of $\theta$, $\mu(b,d,X)$ and the formula beginning with $\forall k$, holds if and only if $b=a^{x}$. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, applied to the functions $\varphi$ and $f$, for all sets $k$, $y$ and $q$: $(k,y)\in\varphi$ if and only if $k\in[n]$ and $y=\varphi(k)$, and $((x,y),q)\in f$ if and only if $(x,y)\in A\times B$ and $q=f(x,y)$. Hence the formula beginning with $\forall k$ says that $(k,f(x,\varphi(k)))\in b$ for every $k\in[n]$. Since $a^{x}$ is a map $[n]\to X$ and $(k,a^{x}(k))\in a^{x}$ for $k\in[n]$ by Functions, Values of a Function, and Functions from One Class to Another §value, $\beta(a^{x})$ holds, 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 §map. Conversely, if $\beta(b)$ holds, then $b$ is a map $b:[n]\to 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 §map, and for $k\in[n]$, $(k,f(x,\varphi(k)))\in b$ gives $b(k)=f(x,\varphi(k))=a^{x}(k)$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value; so $b$ and $a^{x}$ are functions with domain $[n]$ and equal values, and $b=a^{x}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Therefore, for every set $w$, $\theta(w,x)$ holds if and only if $\mathrm{it}(w,n,a^{x})$ does, that is, as $n\in\mathbb{N}$ and $a^{x}$ is a map from $[n]$ to $X$, if and only if $w=\mathop{\ast}\limits_{k=1}^{n}a^{x}_{k}$, where by (V2) the readings of Iterated Operations: Finite Sums and Finite Products §iterated and Iterated Operations: Finite Sums and Finite Products §restriction agree. Now $a^{x}$ is the map $k\mapsto f_{x}(\varphi(k))$ on $[n]$, being the only map on $[n]$ with these values, so $\mathop{\ast}\limits_{k=1}^{n}a^{x}_{k}=\mathop{\ast}\limits_{k=1}^{n}f_{x}(\varphi(k))$ by Iterated Operations: Finite Sums and Finite Products §iterated, and this is $\mathop{\ast}\limits_{y\in B}f_{x}(y)$ by Sums and Products over a Finite Set and over an Interval §operation, applied to $\ast$, $B$, $f_{x}$ and the bijection $\varphi$ from $[\#B]$ onto $B$. It lies in $X$ by (V2). So for every $x\in A$ and every set $w$, $\theta(w,x)$ holds if and only if $w=\mathop{\ast}\limits_{y\in B}f_{x}(y)$, and by (M), with $A$, $X$ and $c(x)=\mathop{\ast}\limits_{y\in B}f_{x}(y)$, there is exactly one map $h:A\to X$ with $h(x)=\mathop{\ast}\limits_{y\in B}f_{x}(y)$ for every $x\in A$.