Nice-name reduction and the ccc counting bound

For every $a\in A$, choose a maximal antichain $A_a$ below $p$ consisting of conditions deciding $\check{a}\in \dot{x}$, retain its positive members $B_a$, and let $\dot{y}=\{⟨\check{a},q⟩:a\in A,q\in B_a\}$. Fix $q\le p$ and $a\in A$. Maximality gives a common extension $r\le q,s$ for some $s\in A_a$. If $s$ is positive, persistence makes $r$ force membership in $\dot{x}$, while the coefficient $s\in B_a$ makes $r$ force membership in $\dot{y}$ by F4. If $s$ is negative, persistence makes $r$ force nonmembership in $\dot{x}$, and incompatibility with every member of $B_a$ leaves no extension of $r$ forcing membership in $\dot{y}$, so the negation clause makes $r$ force nonmembership there. Thus conditions agreeing on the membership of each ground element are dense below $p$. Since $p$ forces $\dot{x}\subseteq \check{A}$ and the displayed coefficients make $\dot{y}$ a name for a subset of $\check{A}$, density closure and the two extensional clauses in F4 give $p⊩\dot{x}=\dot{y}$. The simultaneous maximal-antichain choice is the first use of AC.

Under ccc, each $A_a$ is countable. There are at most ${\mu }^{{\mathrm{\aleph }}_0}$ countable subsets of $P$, so a nice name is coded by a $\lambda$-sequence of such subsets and their number is at most $({\mu }^{{\mathrm{\aleph }}_0}{)}^{\lambda }$. For $A=\omega$, cardinal exponentiation gives $({\mu }^{{\mathrm{\aleph }}_0}{)}^{{\mathrm{\aleph }}_0}={\mu }^{{\mathrm{\aleph }}_0}$. These counts use AC to identify all sets with cardinals.