Proof of Maps from Functional Predicative Relations, and Families of Sections

Throughout, every element of a class is a set (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)).

The relation ((i)). By The Class Comprehension Theorem for Predicative Formulas (i), applied with $n=2$ to $\psi$ and its parameters, there is a class $Z$ such that $\langle u,v\rangle\in Z$ if and only if $\psi(u,v)$, for all sets $u$ and $v$; here $\langle u,v\rangle=(u,v)$ by The Ordered Pair of Two Sets and Nested Tuples (ii). Let $R_{\psi}=Z|_{V}$ be the restriction of $Z$ to the universal class $V$. Its elements are ordered pairs, so it is a relation by Relations, Domain, Range, Inverse and Composition (i); and since every set lies in $V$, for all sets $u$ and $v$ we have $(u,v)\in R_{\psi}$ if and only if $(u,v)\in Z$, that is, if and only if $\psi(u,v)$.

Maps ((ii)). The formula $u\in A\wedge v\in B\wedge\psi(u,v)$ is predicative, with $A$ and $B$ as further class parameters; let $f$ be the relation that (i) gives for it. If $(u,v)\in f$ and $(u,v')\in f$, then $u\in A$, $v,v'\in B$, $\psi(u,v)$ and $\psi(u,v')$, so $v=v'$ by the second hypothesis, and $f$ is a function. Every first component of an element of $f$ lies in $A$, and every $u\in A$ is one, by the first hypothesis; so the domain of $f$ is $A$. Every second component lies in $B$, so the range of $f$ is contained in $B$, and $f:A\to B$ by Functions, Values of a Function, and Functions from One Class to Another (iii). Finally, for $u\in A$ we have $(u,f(u))\in f$ by Functions, Values of a Function, and Functions from One Class to Another (ii), hence $\psi(u,f(u))$.

Families of sections ((iii)). Let $\chi(u,v)$ be the formula $\forall w\,(w\in v\Leftrightarrow(w\in b\wedge(u,w)\in R))$, predicative with the parameters $b$ and $R$ 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 (iii). We check the hypotheses of (ii) for $\chi$, $A$ and $B=\mathcal{P}(b)$. Let $u\in A$. By Axiom of Separation for Classes, applied to the set $b$ and the image $R[\{u\}]$ of the singleton of $u$, there is a set $z$ such that, for every set $w$, $w\in z$ if and only if $w\in b$ and $w\in R[\{u\}]$, that is, since $u$ is the only element of $\{u\}$, if and only if $w\in b$ and $(u,w)\in R$. Thus $\chi(u,z)$ holds, and $z\subseteq b$, so $z\in\mathcal{P}(b)$ by The Union Set and the Power Set of a Set (ii). If $\chi(u,v)$ and $\chi(u,v')$, then $v$ and $v'$ have the same elements, so $v=v'$ by Axiom of Extensionality for Classes. Hence (ii) gives a map $f:A\to\mathcal{P}(b)$ with $\chi(u,f(u))$ for every $u\in A$, which is the displayed property.