Set Theory: Union over sets satisfying criterion, rigorous definition

elementary-set-theorygeneral-topology

I'm trying come to a rigorous understanding of certain types of set unions. For purposes of this question I'm comfortable with set unions written as

$$
\mathcal{A} = \bigcup A = \{x:\exists_a(x\in a \wedge a\in A)\}
$$

but I am not comfortable with unions expressed using other types of notations..

I am trying to understand Munkres Lemma 13.1 concerning a characterization for the basis ($\mathcal{B}$) of a topology*. In fact, I am stuck at the same point as the asker in this question: Proof of Lemma 13.1 in Munkres.

We are considering an open set $U$ and the proof has a step which says for each $x$ in $U$ we know there is a set $B_x$ satisfying $x\in B_x\subset U$ and $B_x \in \mathcal{B}$. I understand and agree with this statement. The next statement is the problem. That statement says that thus

$$
U = \bigcup_{x\in U}B_x
$$

Let

Intuitively I very much understand this statement. We've found a $B_x$ for each $x$ and we combine together all of the $B_x$ that we found. Let

$$
C = \bigcup_{x\in U}B_x
$$

Clearly each $x$ in $U$ will be in this collection so $U\subset C$and clearly each element of this collection is a subset of $U$ so $C\subset U$ so clearly $C=U$.

My problem is understanding what is the rigorous definition of the set $C$ in terms of the definition for infinitary unions I have given above. That is, is there some set $b$ such that I can write

$$
C = \bigcup b
$$

Where $b$ somehow captures the notion of having one set $B_x\subset U$ inside of it for each $x$ in $U$? How would I construct the set $b$ formally? It seems like it is something like constructing a choice function? (something I'm not really familiar with..)

edit:
Just a few notes to explain along what lines I am thinking about the problem. It seems like I want something like

$$
f:U \rightarrow \mathcal{B}
$$

with $x \in f(x) \subset U$. Then I would want $b$ to be the range of $f$ which is guaranteed to be a set by the axiom schema of replacement. The problems are 1) I don't know exactly how to construct the function $f$ and 2) I'm not sure if this is an overkill solution to the issue I am describing when there is in fact a much more straightforward definition..

*However my question doesn't really have to do with this particular proof but rather a general notion about set unions so I don't want to get bogged down in the details of this particular proof.

Best Answer

You can take $$ b = \{B\in \mathcal{B}\colon B\subseteq U\}. $$ Obviously, $$C = \bigcup b\subseteq U.$$ For each $x\in U$ there exists some $B_x\in b$ such that $x\in B_x$, hence $x\in C$.
You don't have to make any choices. You should just take more sets in $b$ than you really need.