Exercise 9.1.15

First, for any $i\in I$, we know that $\left|A_i\right|=\left|A_i^{\prime }\right|$ so that there exists a bijection from $A_i$ onto $A_i^{\prime }$. It was shown in Exercise 2.3.9a that the set $A_i^{\prime {}^{}}exists\; so\; that$ B_i=\{h_i\in A_i^{\prime {}^{}}\}exists\; by\; the\; Axiom\; Schema\; of\; Comprehension.\; Clearly\; then$ B_i\ne \varnothing $for\; every$ i\in I$.\; Since$ B_i$is\; uniquely\; defined\; for\; each$ i\in I$,\; it\; follows\; from\; the\; Axiom\; Schemas\; of\; Replacement\; and\; Comprehension\; that\; the\; set$ \left\{B_i\mid i\in I\right\}$exists,\; which\; is\; a\; system\; of\; nonempty\; sets.\; It\; then\; follows\; from\; Exercise 2.3.9b\; that$ {\prod <!--\; FUNCTION\; APPLICATION\; -->}_{i\in I}{B}_i$exists,\; and\; by\; the\; Axiom\; of\; Choice\; that\; there\; is\; an$ F\in {\prod <!--\; FUNCTION\; APPLICATION\; -->}_{i\in I}{B}_i$,\; i.e.$ F=⟨f_i\mid i\in I⟩$in\; the\; notation\; of\; the\; proof.\; Now$ F$is\; a\; function\; on$ I$in\; which$ F(i)=f_i\in B_i$for\; every$ i\in I$.\; By\; an\; application\; of\; the\; Axiom\; Schema\; of\; Comprehension,$ \mathrm{ran}(F)=\left\{f_i\mid i\in I\right\}$exists,\; and\; we\; have\; that$ f=\bigcup <!--\; FUNCTION\; APPLICATION\; -->\mathrm{ran}(F)$,\; which\; exists\; by\; the\; Axiom\; of\; Union,\; noting\; that\; then$ f={\bigcup <!--\; FUNCTION\; APPLICATION\; -->}_{i\in I}{f}_i$as\; in\; the\; proof.$$