Proof Verification: Lemma 13.1 in Munkres Munkres's Lemma 13.1 states:

Let $X$ be a set; let $\mathcal{B}$ be a basis for a topology $\mathcal{T}$ on $X$. Then $\mathcal{T}$ equals the collection of all unions of elements of $\mathcal{B}$.

If I understand the proof strategy correctly, what I need to show, first, is that every union of basis elements is contained in $\mathcal{T}$, and that every element of $\mathcal{T}$ is in fact a union of basis elements. Here is what I have, if so, which is a slight rewrite of Munkres's proof.

First, I claim that each basis element is an element of $\mathcal{T}$. Indeed, given $B \in \mathcal{B}$ and $x \in B$, we have $x \in B \subset B$ where $B \in \mathcal{B}$, so by definition, $B \in \mathcal{T}$. As $\mathcal{T}$ is a topology, as we just proved, $\bigcup\limits_{B \in \mathcal{B}} B \in \mathcal{T}$. That is, any union of basis elements is contained in $\mathcal{T}$. Next we show that every element of $\mathcal{T}$ is a union of basis elements. Let $U \in \mathcal{T}$. So, given $x \in U$, by definition there exists $B_x \in \mathcal{B}$ such that $x \in B_x \subset U$, which implies that $\bigcup\limits_{x \in U} B_x \subset U$. Conversely, each $x \in U$ is contained in some basis element $B_x$, and hence in $\bigcup\limits_{x \in U} B_x$, so $\bigcup\limits_{x \in U} B_x = U$. So $U$ is a union of basis elements, as desired.

How does this look? Have I correctly understood the proof strategy?
 A: Not quite, in his proof the first thing mentioned is that $\mathcal B \subseteq \mathcal T$ (all basic elements are open in $\mathcal T$) and so unions of subfamilies are in $\mathcal T$ by the definition of a topology. The reverse, that every open set is a union of elements of $\mathcal B$, you do show correctly: all $B_x, x \in U$ are a subset of $U$ hence so is their union, and every $x \in U$ is at least in its $B_x$ so $\bigcup_{x \in U} B_x = U$.
A "choice-free" version of the proof just uses $\mathcal{B}_U =\{B \in \mathcal B\mid B \subseteq U\}$ and then one shows in essentially the same way that $\bigcup \mathcal B_U = U$. This avoids having to "pick" $B_x$ for every $x$ in $U$ and still shows the same thing.
So the first part of your argument is nonsense. The property of being a base for $\mathcal T$ does not ensure that all base members are in $\mathcal T$, we need the extra assumption on the base that they are all open (and this is what Munkres does), otherwise we define a network for the topology, not a base.
Suppose you start with a bare set $X$ and a collection $\mathcal{B}$ satisfying the two axioms (1) and (2), then we can define a new topology $\mathcal{T}$ on $X$ by saying that $\mathcal T$ is the set of all unions of subfamilies of $\mathcal B$. But if we already have a topology $\mathcal{T}$ on $X$ then $\mathcal{B}$ is a base for $\mathcal{T}$ iff $\mathcal{B} \subseteq \mathcal{T}$ and also $\forall U \in \mathcal{T}: \forall x \in U: \exists B \in \mathcal{B}: x \in B \subseteq U$. Then lemma 13.1 says that the given $\mathcal{T}$ is actually equal to the set of all unions of from $\mathcal{B}$ so the base we use to define a topology turns out to be a base for the topology it's defining (!). And then all is well. Lemma 13.2 sort of summarises the situation again.
