Proof of Sets and Functions Defined Componentwise on Families of Vector- and Matrix-Valued Functions

Vectors and matrices as functions. By Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii), $\mathbb{R}^{q}=\mathbb{R}^{[q]}$ and $z_{k}=z(k)$ for $z\in\mathbb{R}^{q}$ and $k\in[q]$. By Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (ii), $\mathcal{M}_{p\times q}(\mathbb{R})=\mathbb{R}^{[p]\times[q]}$ and $M_{ij}=M(i,j)$ for $M\in\mathcal{M}_{p\times q}(\mathbb{R})$, $i\in[p]$ and $j\in[q]$. The elements of $[p]\times[q]$ are exactly the pairs $(i,j)$ with $i\in[p]$ and $j\in[q]$, by The Cartesian Product of Two Classes (i) and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i). Below, $J$ is either $[q]$ or $[p]\times[q]$, and $V=\mathbb{R}^{J}$; so $V=\mathbb{R}^{q}$ in the first case and $V=\mathcal{M}_{p\times q}(\mathbb{R})$ in the second.

The function of components. Let $E=V^{S}\times J$. For $v\in E$, $v=(v_{1},v_{2})$ with $v_{1}\in V^{S}$ and $v_{2}\in J$, by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i); so $v_{1}$ is a function $S\to V$, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), and for $u\in S$, $v_{1}(u)$ is a function $J\to\mathbb{R}$ and $v_{1}(u)(v_{2})\in\mathbb{R}$. Hence there is a function $g:E\times S\to\mathbb{R}$ with $g(v,u)=v_{1}(u)(v_{2})$ for all $v\in E$ and $u\in S$ (Maps and Relations Given by Formulas (ii), with $\mathbb{R}$, $E$ and $S$ for $b$, $c$ and $d$). By Projection, Evaluation and Currying Maps (iii), with $E$, $S$ and $\mathbb{R}$ for $X$, $I$ and $Y$, there is a function $\kappa:E\to\mathbb{R}^{S}$ with $\kappa(v)(u)=g(v,u)$ for all $v\in E$ and $u\in S$. Every function $h:S\to V$ lies in $V^{S}$, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i); so for such $h$ and $w\in J$, $\kappa(h,w)$ is a function $S\to\mathbb{R}$ with $\kappa(h,w)(u)=h(u)(w)$ for every $u\in S$.

For $f:S\to\mathbb{R}^{q}$ and $k\in[q]$ (the case $J=[q]$), $\kappa(f,k)(u)=f(u)(k)=f(u)_{k}$ for every $u\in S$, so $\kappa(f,k)=f_{k}$ by the uniqueness in Component Maps of a Map into $\mathbb{R}^{q}$, Entry Maps of a Map into Matrices, and Maps Assembled from Them (i). For $F:S\to\mathcal{M}_{p\times q}(\mathbb{R})$, $i\in[p]$ and $j\in[q]$ (the case $J=[p]\times[q]$), $\kappa(F,(i,j))(u)=F(u)(i,j)=F(u)_{ij}$ for every $u\in S$, so $\kappa(F,(i,j))=F_{ij}$ by the uniqueness in Component Maps of a Map into $\mathbb{R}^{q}$, Entry Maps of a Map into Matrices, and Maps Assembled from Them (ii).

Proof of (i) and (iii). Let $D$ and $A$ be as in (i), with $J=[q]$, or as in (iii), with $J=[p]\times[q]$. Then $D\subseteq V^{S}$, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i). Let

$$Z=\{h\in D:\forall w\,(w\in J\Rightarrow\kappa(h,w)\in A)\},$$

a set (Sets and Maps: Ordinary Notation (iii)). By the previous paragraph, and as $w$ runs through the pairs $(i,j)$ when $J=[p]\times[q]$, the elements of $Z$ are exactly the $f\in D$ with $f_{k}\in A$ for every $k\in[q]$ in the first case, and exactly the $F\in D$ with $F_{ij}\in A$ for all $i\in[p]$ and $j\in[q]$ in the second. A set $Z'$ with the same elements has the elements of $Z$, so $Z'=Z$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (ii).

Proof of (ii) and (iv). Let $D$, $A$, $Z$, $B$ and $\Phi$ be as in (ii), with $J=[q]$, or as in (iv), with $J=[p]\times[q]$. For $h\in Z$ and $w\in J$, $\kappa(h,w)\in A$ by the construction of $Z$ above, so $\Phi(\kappa(h,w))\in B$. Hence there is a function $\psi:Z\times J\to B$ with $\psi(h,w)=\Phi(\kappa(h,w))$ for all $h\in Z$ and $w\in J$ (Maps and Relations Given by Formulas (ii), with $B$, $Z$ and $J$ for $b$, $c$ and $d$), and, by Projection, Evaluation and Currying Maps (iii) with $Z$, $J$ and $B$ for $X$, $I$ and $Y$, exactly one function $\Psi:Z\to B^{J}$ with $\Psi(h)(w)=\psi(h,w)$ for all $h\in Z$ and $w\in J$. By the identification of $\kappa$ above, this says $\Psi(f)(k)=\Phi(f_{k})$ for all $f\in Z$ and $k\in[q]$ in the first case, and $\Psi(F)(i,j)=\Phi(F_{ij})$ for all $F\in Z$, $i\in[p]$ and $j\in[q]$ in the second. Conversely, let $\Psi':Z\to B^{J}$ be a function with the property stated in (ii), respectively (iv). As every $w\in[p]\times[q]$ is a pair $(i,j)$ with $i\in[p]$ and $j\in[q]$, $\Psi'(h)(w)=\Phi(\kappa(h,w))=\psi(h,w)$ for all $h\in Z$ and $w\in J$, so $\Psi'=\Psi$ by the uniqueness in Projection, Evaluation and Currying Maps (iii).