Is the axiom of choice used in the proof that every open set is the union of basis elements (Mukres, Lemma 13.1)

This is phrased in such a way as to invoke AC. However, it doesn't have to be: given an open set $U$, consider $$\mathfrak{A}=\{A\in\mathcal{B}: A\subseteq U\}.$$ Since $\mathcal{B}$ is a basis we have $\bigcup\mathfrak{A}=U$, and we didn't need to use choice anywhere.

There is an interesting feature here, however: the number of elements of $\mathcal{B}$ we need. The choice-y version lets us get by with at most $\vert U\vert$-many, namely one for each point; this approach, however, is only bounded by the number of subsets of $U$, that is, by $2^{\vert U\vert}$. So the choice-flavored question here is the following:

Is it consistent with $\mathsf{ZF}$ (= set theory without choice) that there is a topological space $(X,\mathcal{T})$, a basis $\mathcal{B}$ for $\mathcal{T}$, and an open set $U\in\mathcal{T}$ such that $U$ cannot be covered by "$U$-many" basis elements - that is, such that there is no map $f:U\rightarrow\mathcal{B}$ with $$U=\bigcup_{x\in U}f(x)?$$

Note the care I'm taking vis-a-vis the notion of "$U$-many" - without choice, we have to be careful whenever we want to talk about cardinalities.

It turns out that the answer is yes. Set-theoretic independence proofs are extremely hard, but very roughly: we just put infinitely many cofinite topologies next to each other ... but, like, really pathologically.

In a bit, but really only a bit, more detail: fixing a "really-unchoicey" sequence $\mathfrak{X}=(X_i)_{i\in\mathbb{N}}$ of disjoint sets, let $X=\bigcup_{i\in\mathbb{N}}X_i$, let $\mathcal{B}_i=\{A\subseteq X_i: \vert X_i\setminus A\vert\ge 2\}$, and let $$\mathcal{B}=\bigcup_{i\in\mathbb{N}}\mathcal{B}_i.$$ Now $\mathcal{B}$ is a basis for the topology $\mathcal{T}$ it generates; set $U=X$.

By the "really-unchoiciness" of $\mathfrak{X}$, every $\mathcal{C}\subseteq\mathcal{B}$ with $\bigcup\mathcal{C}=X$ is "essentially" all of $\mathcal{B}$. More precisely, we have $\mathcal{C}\supseteq\mathcal{B}_i$ for all but finitely many $i$s. But by a second application of "really-unchoiciness" - essentially that there are many more pairs of elements of $X_i$ than there are elements of $X_i$ - we can show that there is no surjection from $X$ onto any such $\mathcal{C}$ (this is where the "$\ge 2$" comes in).

Note that in this last bit, I'm assuming that the $X_i$s are also "really-unchoicey." For example, it's enough to demand that they each be amorphous (a set is amorphous iff it is infinite but cannot be partitioned into two infinite subsets), although this is overkill.

Of course I haven't tried to justify any of the above (why is the existence of such a $\mathfrak{X}$ consistent with $\mathsf{ZF}$ in the first place?), but it does work.

If you're familiar with forcing and symmetric submodels, I believe this happens in a version of Cohen's original model of $\mathsf{ZF+\neg AC}$: let $A$ be the infinite Dedekind-finite set of generic reals added, and let $X_i=A\cap [i, i+1]$. Admittedly I haven't checked the details on this one, but I believe this is the simplest model exhibiting such a $\mathfrak{X}$. Note of course that these $X_i$s are not amorphous, since no linearly orderable set can be amorphous.

That, in turn, raises one final choice-y question:

Over $\mathsf{ZF}$, how strong is the statement "For every topological space $(X,\mathcal{T})$, every basis $\mathcal{B}$ for $\mathcal{T}$, and every $U\in\mathcal{T}$, there is some function $f:U\rightarrow\mathcal{B}$ with $U=\bigcup_{x\in U}f(u)$?

For example, does it imply full choice?

I tentatively suspect that it does, in fact, but I don't see how to prove it. Maybe one of our other resident set theorists will pipe up with the answer. :P

EDIT: I've asked about this on MSE, and subsequently on MO.

This proof might, but I think we can do without choice with some modification.

I claim that for any $U \in \mathcal T$, $U$ is the union of all sets $B \in \mathcal B$ such that $B \subseteq U$.

Clearly $U$ contains this union, since it contains every set we're unioning. To see the converse, we should check that for every $x \in U$, $x$ is also an element of this union. And this is where $B_x$ comes in: for every $x \in U$, there is a $B_x$ such that $x \in B_x$ and $B_x \subseteq U$.

Yes, in this argument the Axiom of Choice is used, but you can avoid it.

For all $U \in T$, call $$\mathcal{A}= \{ B \in \mathcal{B} : B \subseteq U \}$$ Clearly, $\bigcup \mathcal{A} \subseteq U$. The converse inclusion can be showed by contradiction, without using the Axiom of Choice: for all $x \in U \setminus \bigcup \mathcal{A}$, there exists $B_x \in \mathcal{B}$ such that $x \in B_x \subseteq U$ (by definition of $U \in T$). But then, $B_x \in \mathcal{A}$, hence $x \in B_x \subseteq \bigcup \mathcal{A}$: a contradiction.