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

Predicativity. Let $s$ and $f$ be set variables distinct from each other and from $q$ and $S$. Let $\mathrm{seg}(s,q)$ be the predicative formula of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), with $s$ and $q$ for its set variables and $Y$ and $R$ for its class variables, so that for every set $s$ and every $n\in\mathbb{N}_{0}$, $\mathrm{seg}(s,n)$ holds if and only if $s=[n]$. Let $\beta(f,s,S)$ be the predicative 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 (x), with $f$, $s$ and $S$ for its variables $F$, $A$ and $B$, as 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) permits; it holds if and only if $f$ is a bijection from $s$ to $S$. Put

$$\kappa(q,S)\;=\;q\in X\wedge\exists s\,\exists f\,\bigl(\mathrm{seg}(s,q)\wedge\beta(f,s,S)\bigr).$$

It is predicative, since it adds to predicative formulas only connectives and quantifiers over set variables, and its free variables are among $q$, $S$, $X$, $Y$ and $R$.

Let $n$ and $B$ be sets. If $\kappa$ holds for them, then $n\in\mathbb{N}_{0}$, and there are a set $s$ with $s=[n]$ and a bijection $f$ from $[n]$ onto $B$; so $B$ is finite by Finite Sets (i), and $n=\#B$ by The Number of Elements of a Finite Set (i). Conversely, if $B$ is finite and $n=\#B$, then $n\in\mathbb{N}_{0}$ and there is a bijection $f$ from $[n]$ onto $B$ by The Number of Elements of a Finite Set (i); with $s=[n]$, which satisfies $\mathrm{seg}(s,n)$, $\kappa$ holds. This proves (iii).

In particular, for a finite set $B$ exactly one set $q$ satisfies $\kappa(q,B)$, namely $\#B$, the length being unique by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (ii). Hence Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii), with $\theta=\kappa$ and with $\gamma(S)=\mathrm{fin}(S)$, the predicative formula of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii) (whose class variables are assigned $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$ as here), lets $\#S$ be eliminated through $\kappa$ from every predicative formula, for every finite set $S$.

Counting a family. For $i\in I$, the value $C_{i}$ is a defined set symbol used properly (Functions, Values of a Function, and Functions from One Class to Another (ii)), and $\#C_{i}$ is used properly by this elimination, because $C_{i}$ is finite; moreover $\#C_{i}\in\mathbb{N}_{0}$ by The Number of Elements of a Finite Set (i). Hence Maps and Relations Given by Formulas (i), applied to the expression $\#C_{i}$ with the parameters $C$, $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$, gives exactly one map $c:I\to\mathbb{N}_{0}$ with $c(i)=\#C_{i}$ for every $i\in I$. This proves (i).

Counting subsets. Every $S\in\mathcal{P}(A)$ is a subset of $A$ by The Union Set and the Power Set of a Set (ii), hence finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv), so $\#S$ is used properly by the same elimination and lies in $\mathbb{N}_{0}$. As before, Maps and Relations Given by Formulas (i), applied to the expression $\#S$ on the set $\mathcal{P}(A)$, gives exactly one map $\mathcal{P}(A)\to\mathbb{N}_{0}$ with value $\#S$ at every $S\in\mathcal{P}(A)$. This proves (ii).