Equivalent formulation of coarseness of two topologies + Axiom of Choice The problem: If $\tau_1$ and $\tau_2$ are topologies, show that $\tau_1 \subseteq \tau_2 \iff \forall U \in \tau_1 \: \forall x \in U \; \exists V \in \tau_2 (x \in V \subseteq U).$ Try not to use the axiom of choice.
I was able to solve the problem easily with the axiom of choice, but I am really struggling to find a way to avoid using it. My issue is it seems to be the case that, to even assume the condition on the right hand side in the first place, we need to invoke AC. If not, then how are we guarunteed a mapping between the sets $\{x \mid x \in U\}$ and $\{V \in \tau_2 \mid x \in V \subseteq U\}.$ My understanding of set theory doesn't run very deep, so let me know if there's some fundamental misunderstanding I'm having here, or if I'm not being precise enough.
 A: If $U\in\tau_1,$ then we have $$ U = \bigcup\{V\in \tau_2:  V\subseteq U\}.$$ It's clear that the RHS is a subset of $U,$ and the fact that for all $x\in U$ there is a $V\subseteq U$ such that $V\in\tau_2$ and $x\in V$ gives the other inclusion. The RHS is clearly in $\tau_2,$ so $U\in \tau_2$ and $\tau_1\subseteq \tau_2.$ (The other direction of the iff is trivial.)
There is no use of choice here. The only issue is really the temptation to try to establish a mapping between the $x\in U$ and "the corresponding $V$" when there is no need for one. You'd need choice to make such a mapping (since there is no such thing as "the" corresponding $V$), but again, there's no need for the mapping in the first place.
EDIT
I read your question a little more carefully and will address your misconception more directly:

My issue is it seems to be the case that, to even assume the condition on the right hand side in the first place, we need to invoke AC.

No. We don't need AC to make sense of a statement like $\forall x\exists y\varphi(x,y)$. AC is used to make a function, $f$ such that $\forall x \varphi(x,f(x)),$ should we want or need such a thing.
$\forall x\exists y\varphi(x,y)$ means that for every $x$ we can find some $y$ such that $\varphi(x,y)$ holds. If we wanted to use this fact to construct a function $f$ such that $\forall x \varphi(x,f(x))$, we would need to invoke it infinitely many times, once for each value of $x.$ This is not possible to do within a span of a finite proof, so we need AC to tell us such a function exists (provided we can't define some canonical such function).
But, as I said above, we don't need such a function in order to make sense of $\forall x\exists y\varphi(x,y)$ or to prove $ U \subseteq \bigcup\{V\in \tau_2:  V\subseteq U\}$ above. For that, we just argue as follows:

Let $x\in U.$ Let $V\in \tau_2$ such that $x\in V\subseteq U.$ Then $x\in V,$ where $V\in \tau_2$ and $V\subseteq U,$ so $x\in \bigcup\{V\in \tau_2:  V\subseteq U\}.$

A: In the statement
$$\forall U \in \tau_1: \forall x \in U: \exists V \in \tau_2: x \in V \subseteq U\tag{1}$$
we are not suggesting a mapping from $\tau_1 \times X$ to $\tau_2$ exists. It's just a statement of logic, not a statement that some set (a mapping is a set of a special type) exists at all.
A: It holds that $\tau_1\subseteq\tau_2$ if and only if the identity on $X$ is a continuous function $\hat{id}:(X,\tau_2)\rightarrow(X,\tau_1)$. A map is continuous if and only if it is continuous at each point of its domain. Thus $\hat{id}$ is continuous if and only if for each $x\in X$ and each (open) neighbourhood $U\in\tau_1$ of $\hat{id}(x)=x$, there is $V\in\tau_2$ with $x\in V$ and $\hat{id}(V)=V\subseteq U$.
A: *

*(Simple). If $\tau_1\subset \tau_2:$ Just let $V=U$. Because if  $U\in \tau_1\subseteq \tau_2$  then $U\in \tau_2.$


*If the RHS in the Q holds: One of the profs on this site quoted the adage "If you have no Choice, choose everything."
For any $U\in \tau_1$ there exist $A_U=\{V\in \tau_2: V\subseteq U\}$ and $B_U=\bigcup A_U.$
Clearly $$(*)\quad B_U\in \tau_2$$ and $$(**)\quad B_U\subseteq U.$$ Now for any $x\in U$ there exists (by hypothesis) $V\in \tau_2$ with $x\in V\subseteq U,$ so there exists $V$ with $x\in V\in  A_U,$ so $x\in \bigcup A_U=B_U$ by the definition of $\bigcup.$
So $$(***)\quad U\subseteq B_U.$$
By $(**)$ and $(***)$ we have $U=B_U,$ so by $(*)$ we have $U\in \tau_2.$
Remark: Each $A_U$ exists by the Axiom Schema of Comprehension.
