My question is pretty straight forward - how do I use ZF axioms to prove that if $\{A\}_{i\in\Bbb{N}}$ is a family of sets, then $\bigcap_{i}A_i$ is a set?
I feel like I should be using the axiom of union and the axiom of separation, but I'm not quite sure how.
On
They way I learned it (I believe this is how Halmos gives it, but he isn’t writing a fully formal presentation of $\mathsf{ZF}$), the Axiom of Union guarantees the existence of the unary union. We know that for all $X$ there exists $A$ such that $$\forall z\Bigl(\bigl(\exists y (y\in X\wedge z\in y)\bigr)\longrightarrow z\in A\Bigr).$$ and then with Separation we can define $$\bigcup X = \{z\mid \exists y(y\in X\wedge z\in y)\}.$$ Once we have defined the (unary) union, we define the unary intersection by $$\bigcap X = \left\{z\in \bigcup X\Bigm| \forall y (y\in X\longrightarrow z\in y)\right\}$$ which is a set by the Axiom of Separation.
Note that with this definition, you would get that the empty intersection is empty; some people don’t like that (and there are good reasons for avoiding it, and good reasons for not minding or even wishing that). In any case, you can use the latter definition to conclude that $\bigcap X$ is a set in $\mathsf{ZF}$ for any particular nonempty $X$.
To be precise, we must prove the following statement:
For all non-empty $I$, for all index families $\{A_i\}_{i \in I}$, there exists a unique set $S$ such that for all $x$, $x \in S \iff \forall i, x \in A_i$.
To prove this, suppose we such an $I$ and a family $A$. Then let $j$ be an element of $I$. Then by the axiom of separation, there exists $S$ such that for all $x$, $x \in S \iff x \in A_j \land \forall i \in I, x \in A_i$. We then immediately see that for all $x$, $x \in S \iff \forall i \in I, x \in A_i$. Thus, we have shown existence.
For uniqueness, we note that if we have two such sets $S$ and $S'$, then for all $x$, $x \in S \iff (\forall i \in I, x \in A_i) \iff x \in S'$ and hence $S = S'$ by the axiom of extensionality.