The Maps i ↦ #C(i) and S ↦ #S

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let finite sets be as in Finite Sets (i), $\#$ as in The Number of Elements of a Finite Set (i), and $\mathcal{P}(A)$ the power set of a set $A$.

(i) Counting a family. Let $I$ be a set and $(C_{i})_{i\in I}$ a family of finite sets. There is exactly one map $c:I\to\mathbb{N}_{0}$ with $c(i)=\#C_{i}$ for every $i\in I$.

(ii) Counting subsets. Let $A$ be a finite set. There is exactly one map $\mathcal{P}(A)\to\mathbb{N}_{0}$ whose value at every $S\in\mathcal{P}(A)$ is $\#S$.

(iii) Predicativity. This clause is a statement of the metatheory. Let $q$ and $S$ be distinct set variables and $X$, $Y$ and $R$ distinct class variables, assigned $\mathbb{N}_{0}$, $\mathbb{N}$ and the order $\le$ of $\mathbb{N}_{0}$, respectively. There is a predicative formula $\kappa(q,S)$, whose free variables are among $q$, $S$, $X$, $Y$ and $R$, such that for all sets $n$ and $B$, $\kappa$ holds when $n$ and $B$ are assigned to $q$ and $S$ if and only if $B$ is finite and $n=\#B$.