= Double-power-set countability bound without choice
{title2=$|A|\text{ nonfinite}\Longrightarrow\aleph_0<|\mathcal P(\mathcal P(A))|$}
For each <natural number> $n$, the family $[A]^n$ of all $n$-element subsets is nonempty when $A$ is not finite. These families are pairwise distinct elements of $\mathcal P(\mathcal P(A))$, giving an explicit <injection> of the <natural numbers>. No representative from each family is selected. A <power set> cannot be countably infinite in ZF: if $\mathcal P(B)$ were countably infinite, singleton <injection> would make $B$ an infinite subset of a <countable> set and hence countably infinite; <Cantor's theorem> would then contradict countability of its <power set>. Apply this to $B=\mathcal P(A)$ to make the displayed lower bound strict.
Back to article page
