Proof of Partial Iterates of a Two-Variable Map, Row by Row and Column by Column

Formulas. The formulas below are formulas of class theory as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii), written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi) and read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv). 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 below is built from parts shown predicative where it is introduced, by the connectives and by quantifiers over set variables; so no quantifier is applied to a class variable in it, and it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Values. (V) For sets $D_{1}$, $D_{2}$ and $E$, a map $F:D_{1}\times D_{2}\to E$, $u\in D_{1}$ and $v\in D_{2}$: $(u,v)\in D_{1}\times D_{2}$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i), so $F(u,v)=F((u,v))$ is used properly and lies in $E$, and for every set $z$, $((u,v),z)\in F$ if and only if $z=F(u,v)$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii). Finally, for every $N\in\mathbb{N}$, $[N]$ is a set and $[N]=\{k\in\mathbb{N}:k\le N\}\subseteq\mathbb{N}$, by Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices (v), every element of $[N]$ being a natural number by Elements of a Segment Are Natural Numbers, and Mixed Transitivity of the Order on the Natural Numbers (i).

Maps from formulas in two variables. We use the following form (M2) of Maps and Relations Given by Formulas (ii). Let $C$, $D$ and $V$ be sets, let a set $c(v,u)\in V$ be given for all $v\in C$ and $u\in D$, and let $\theta(z,v,u)$ be a predicative formula, with $z$, $v$ and $u$ distinct set variables and its parameters assigned, such that for all $v\in C$, $u\in D$ and every set $z$, $\theta(z,v,u)$ holds if and only if $z=c(v,u)$. Then there is exactly one map $g:C\times D\to V$ with $g(v,u)=c(v,u)$ for all $v\in C$ and $u\in D$. Indeed, for $v\in C$ and $u\in D$ exactly one set $z$ satisfies $\theta(z,v,u)$, namely $c(v,u)$; so the set $\tau(v,u)$ with $\theta(\tau(v,u),v,u)$ is a defined set symbol given by $\theta$, with the set arguments $v$ and $u$, as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii), used properly wherever $v\in C$ and $u\in D$ are in force, as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii) with $\gamma(v,u)$ the formula $v\in C\wedge u\in D$, $C$ and $D$ being assigned to further parameters; and $\tau(v,u)=c(v,u)\in V$. By Maps and Relations Given by Formulas (ii), applied to the sets $V$, $C$ and $D$ and the expression $\tau(v,u)$, there is exactly one map $g:C\times D\to V$ with $g((v,u))=\tau(v,u)=c(v,u)$ for all $v\in C$ and $u\in D$.

The map with swapped arguments. We prove (iii). Let $f:A\times B\to X$ be given, assigned to a class variable $G$. Let $\theta(z,y,x)$ be the formula $((x,y),z)\in G$; it 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 (iv), which also says that, for sets $x$, $y$ and $z$, it holds if and only if $((x,y),z)\in f$. So for all $y\in B$, $x\in A$ and every set $z$, $\theta(z,y,x)$ holds if and only if $z=f(x,y)$, and $f(x,y)\in X$, by (V). By (M2), with $B$, $A$, $X$ and $c(y,x)=f(x,y)$, there is exactly one map $h:B\times A\to X$ with $h(y,x)=f(x,y)$ for all $x\in A$ and $y\in B$.

The formula for iterated operations. Assign $X$, $\ast$, $\mathbb{N}$, the order $\le$ of $\mathbb{N}_{0}$ and the addition $+$ of $\mathbb{N}_{0}$ to the distinct class variables $X$, $F$, $Y$, $R$ and $P$, respectively, of Iterated Operations Are Given by a Predicative Formula (i). For 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$, $R$ 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}$, which is the iterated operation of $b|_{[N]}$ by Iterated Operations: Finite Sums and Finite Products (ii).

Iterates along the second argument. We prove (i). Let $f:A\times\mathbb{N}\to X$ be given, assigned to a class variable $G$ other than $X$, $F$, $Y$, $R$ and $P$.

The sections $f_{x}$. For $x\in A$ and $k\in\mathbb{N}$, $f(x,k)$ is used properly and lies in $X$, by (V); for $x\in A$ let $f_{x}:\mathbb{N}\to X$ be the map $k\mapsto f(x,k)$ of Sets and Maps: Ordinary Notation (v). Apply Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v) with the sets $\mathbb{N}$ and $X$, assigned to $Y$ and $X$, in place of its sets $A$ and $B$; with one variable $v_{1}$, namely $x$; with the set variables $k$ and $b$ in place of $u$ and $h$; with $\gamma(x)$ the formula $x\in A$; and with $t(k,x)$ the expression $f(x,k)$, that is $G((x,k))$, built from variables and defined set symbols with no class abstraction written in it. For every $x\in A$ and every $k\in\mathbb{N}$, $t(k,x)$ is used properly and lies in $X$, as just shown; the parameters are $Y$, $X$, $A$ and $G$, and $b$ occurs in neither $\gamma$ nor $t$. Let $\beta(b,x)$ be the formula $\theta(b,x)$ of that clause, namely $\mu(b,Y,X)\wedge\forall k\,(k\in Y\Rightarrow(k,G((x,k)))\in b)$, 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 (vii). By that clause, $\beta$ is predicative, and for every $x\in A$ the only set $b$ satisfying $\beta(b,x)$ is $f_{x}$.

The partial iterates. Let $\theta(w,N,x)$ be $\exists b\,(\beta(b,x)\wedge\mathrm{it}(w,N,b))$, which is predicative, its parts being so: $\beta(b,x)$ by the preceding paragraph, and $\mathrm{it}(w,N,b)$ by the paragraph on the formula for iterated operations, used here with the set variables $w$, $N$ and $b$ (a predicative formula stays predicative when its free set variables are renamed, 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 (i)). Let $N\in\mathbb{N}$ and $x\in A$. The map $f_{x}$ is a set, being a map between the sets $\mathbb{N}$ and $X$, by Sets and Maps: Ordinary Notation (v); so by the preceding paragraph, for every set $w$, $\theta(w,N,x)$ holds if and only if $\mathrm{it}(w,N,f_{x})$ does, that is, as $f_{x}$ is a map from $\mathbb{N}\supseteq[N]$ to $X$, if and only if $w=\mathop{\ast}\limits_{k=1}^{N}(f_{x})_{k}$, the iterated operation of $f_{x}|_{[N]}$. For $k\in[N]\subseteq\mathbb{N}$, $f(x,k)\in X$ by (V), so the map $\varphi:[N]\to X$, $k\mapsto f(x,k)$, of Sets and Maps: Ordinary Notation (v) is defined. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix), $f_{x}|_{[N]}$ is a function with domain $[N]\cap\mathbb{N}=[N]$ and value $f_{x}(k)=f(x,k)=\varphi(k)$ at each $k\in[N]$, so $f_{x}|_{[N]}=\varphi$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i). Hence $\mathop{\ast}\limits_{k=1}^{N}(f_{x})_{k}$ is the iterated operation of $\varphi$, which is $\mathop{\ast}\limits_{n=1}^{N}f(x,n)$ by Iterated Operations: Finite Sums and Finite Products (i), and it lies in $X$ (by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set (i), applied to $\varphi$). So for all $N\in\mathbb{N}$, $x\in A$ and every set $w$, $\theta(w,N,x)$ holds if and only if $w=\mathop{\ast}\limits_{n=1}^{N}f(x,n)$, and by (M2), with $\mathbb{N}$, $A$, $X$ and $c(N,x)=\mathop{\ast}\limits_{n=1}^{N}f(x,n)$, there is exactly one map $g:\mathbb{N}\times A\to X$ with $g(N,x)=\mathop{\ast}\limits_{n=1}^{N}f(x,n)$ for all $N\in\mathbb{N}$ and $x\in A$.

Iterates along the first argument. We prove (ii). Let $f:\mathbb{N}\times A\to X$ be given. By (iii), applied to the sets $\mathbb{N}$ and $A$ in place of $A$ and $B$, there is a map $h:A\times\mathbb{N}\to X$ with $h(y,m)=f(m,y)$ for all $m\in\mathbb{N}$ and $y\in A$. Let $N\in\mathbb{N}$ and $y\in A$. For $m\in[N]\subseteq\mathbb{N}$, $h(y,m)=f(m,y)\in X$ by (V), so the maps $m\mapsto h(y,m)$ and $m\mapsto f(m,y)$ on $[N]$, of Sets and Maps: Ordinary Notation (v), are defined; they are functions with domain $[N]$ and equal values, so they are equal by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i), and therefore $\mathop{\ast}\limits_{m=1}^{N}h(y,m)=\mathop{\ast}\limits_{m=1}^{N}f(m,y)$ by Iterated Operations: Finite Sums and Finite Products (i). Hence a map $g:\mathbb{N}\times A\to X$ satisfies $g(N,y)=\mathop{\ast}\limits_{m=1}^{N}f(m,y)$ for all $N\in\mathbb{N}$ and $y\in A$ if and only if it satisfies $g(N,y)=\mathop{\ast}\limits_{m=1}^{N}h(y,m)$ for all $N\in\mathbb{N}$ and $y\in A$; by (i), applied to $h$, there is exactly one such map.