The k-Element Subsets of a Set

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $A$ be a set and $k\in\mathbb{N}_{0}$, and for a finite set $S$ let $\#S$ be its number of elements.

(i) The $k$-element subsets. The set of $k$-element subsets of $A$ is

$$\mathcal{P}_{k}(A)=\{S\in\mathcal{P}(A):S\text{ is finite and }\#S=k\},$$

a subset of the power set $\mathcal{P}(A)$ and hence a set (the condition is predicative by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii) and The Maps i ↦ #C(i) and S ↦ #S (iii)).

(ii) Membership. For a set $S$, $S\in\mathcal{P}_{k}(A)$ if and only if $S\subseteq A$, $S$ is finite and $\#S=k$, the elements of $\mathcal{P}(A)$ being the subsets of $A$ by The Union Set and the Power Set of a Set (ii).