[proofplan]
We verify the three topology axioms directly from the defining local condition for $\tau_{\mathcal B}$. The covering axiom for the basis gives $X \in \tau_{\mathcal B}$, while the empty set satisfies the condition vacuously. Arbitrary unions are handled by choosing the member of the union containing the point, and finite intersections are handled using the basis refinement axiom. Finally, the same local basis elements used in the definition show that each $U \in \tau_{\mathcal B}$ is exactly a union of elements of $\mathcal B$.
[/proofplan]
[step:Verify that $\varnothing$ and $X$ belong to $\tau_{\mathcal B}$]
The set $\varnothing$ belongs to $\tau_{\mathcal B}$ because the defining condition
\begin{align*}
\text{for every } x \in \varnothing, \text{ there exists } B \in \mathcal B \text{ such that } x \in B \subset \varnothing
\end{align*}
is vacuously true.
Next let $x \in X$. Since $\mathcal B$ is a basis on $X$, its elements cover $X$, so there exists $B_x \in \mathcal B$ such that $x \in B_x$. Because every element of $\mathcal B$ is a subset of $X$, we have $x \in B_x \subset X$. Hence $X \in \tau_{\mathcal B}$.
[/step]
[step:Show that arbitrary unions of elements of $\tau_{\mathcal B}$ remain in $\tau_{\mathcal B}$]
Let $I$ be an index set, and let $(U_i)_{i \in I}$ be a family of subsets of $X$ such that $U_i \in \tau_{\mathcal B}$ for every $i \in I$. Define
\begin{align*}
U := \bigcup_{i \in I} U_i.
\end{align*}
We prove that $U \in \tau_{\mathcal B}$.
Let $x \in U$. By the definition of indexed union, there exists $i_x \in I$ such that $x \in U_{i_x}$. Since $U_{i_x} \in \tau_{\mathcal B}$, there exists $B_x \in \mathcal B$ such that
\begin{align*}
x \in B_x \subset U_{i_x}.
\end{align*}
Because $U_{i_x} \subset U$, it follows that
\begin{align*}
x \in B_x \subset U.
\end{align*}
Thus every point of $U$ is contained in a basis element lying inside $U$, so $U \in \tau_{\mathcal B}$.
[guided]
We need to prove that the union satisfies the same local condition that defines $\tau_{\mathcal B}$. Let $I$ be an index set, and let $(U_i)_{i \in I}$ be a family with $U_i \in \tau_{\mathcal B}$ for every $i \in I$. Define the union
\begin{align*}
U := \bigcup_{i \in I} U_i.
\end{align*}
Take an arbitrary point $x \in U$. The meaning of $x \in \bigcup_{i \in I} U_i$ is that $x$ lies in at least one member of the family, so there exists an index $i_x \in I$ such that $x \in U_{i_x}$. Now we use the hypothesis $U_{i_x} \in \tau_{\mathcal B}$. By the definition of $\tau_{\mathcal B}$, there exists a basis element $B_x \in \mathcal B$ satisfying
\begin{align*}
x \in B_x \subset U_{i_x}.
\end{align*}
Since $U_{i_x}$ is one of the sets included in the union, we have $U_{i_x} \subset U$. Therefore
\begin{align*}
x \in B_x \subset U.
\end{align*}
Because $x \in U$ was arbitrary, every point of $U$ has a basis element around it contained in $U$. This is exactly the defining condition for $U \in \tau_{\mathcal B}$.
[/guided]
[/step]
[step:Use the basis refinement axiom to prove closure under finite intersections]
It suffices to prove closure under binary intersections, since closure under all finite intersections follows by induction and since $X \in \tau_{\mathcal B}$ gives the empty finite intersection.
Let $U,V \in \tau_{\mathcal B}$. We prove that $U \cap V \in \tau_{\mathcal B}$. Let $x \in U \cap V$. Since $U \in \tau_{\mathcal B}$, there exists $B_U \in \mathcal B$ such that
\begin{align*}
x \in B_U \subset U.
\end{align*}
Since $V \in \tau_{\mathcal B}$, there exists $B_V \in \mathcal B$ such that
\begin{align*}
x \in B_V \subset V.
\end{align*}
Then $x \in B_U \cap B_V$. By the basis refinement axiom applied to $B_U$, $B_V$, and $x$, there exists $B_x \in \mathcal B$ such that
\begin{align*}
x \in B_x \subset B_U \cap B_V.
\end{align*}
Since $B_U \subset U$ and $B_V \subset V$, we have
\begin{align*}
B_U \cap B_V \subset U \cap V.
\end{align*}
Consequently
\begin{align*}
x \in B_x \subset U \cap V.
\end{align*}
Thus $U \cap V \in \tau_{\mathcal B}$, and therefore $\tau_{\mathcal B}$ is closed under finite intersections.
[guided]
The only non-formal topology axiom is closure under finite intersections, because intersecting two neighbourhoods may make them smaller. The basis refinement axiom is exactly designed to handle this.
First, it is enough to prove closure under intersections of two sets. Once binary intersections are known, any finite intersection follows by induction:
\begin{align*}
U_1 \cap \cdots \cap U_n = (U_1 \cap \cdots \cap U_{n-1}) \cap U_n.
\end{align*}
The empty finite intersection is $X$, which has already been shown to lie in $\tau_{\mathcal B}$.
Let $U,V \in \tau_{\mathcal B}$, and take an arbitrary point $x \in U \cap V$. Since $x \in U$ and $U \in \tau_{\mathcal B}$, the definition of $\tau_{\mathcal B}$ gives a basis element $B_U \in \mathcal B$ such that
\begin{align*}
x \in B_U \subset U.
\end{align*}
Similarly, since $x \in V$ and $V \in \tau_{\mathcal B}$, there exists $B_V \in \mathcal B$ such that
\begin{align*}
x \in B_V \subset V.
\end{align*}
Now $x$ lies in the intersection $B_U \cap B_V$ of two basis elements. The basis refinement axiom says that whenever two basis elements meet at a point, there is a smaller basis element around that point contained in their intersection. Applying this axiom to $B_U$, $B_V$, and $x$, we obtain $B_x \in \mathcal B$ such that
\begin{align*}
x \in B_x \subset B_U \cap B_V.
\end{align*}
Because $B_U \subset U$ and $B_V \subset V$, their intersection satisfies
\begin{align*}
B_U \cap B_V \subset U \cap V.
\end{align*}
Combining the inclusions gives
\begin{align*}
x \in B_x \subset U \cap V.
\end{align*}
Since $x \in U \cap V$ was arbitrary, every point of $U \cap V$ has a basis element contained in $U \cap V$. Hence $U \cap V \in \tau_{\mathcal B}$, and consequently $\tau_{\mathcal B}$ is closed under finite intersections.
[/guided]
[/step]
[step:Conclude that $\tau_{\mathcal B}$ is a topology on $X$]
By the preceding steps, $\varnothing \in \tau_{\mathcal B}$ and $X \in \tau_{\mathcal B}$, arbitrary unions of elements of $\tau_{\mathcal B}$ belong to $\tau_{\mathcal B}$, and finite intersections of elements of $\tau_{\mathcal B}$ belong to $\tau_{\mathcal B}$. These are precisely the axioms in the definition of a [topology](/page/Topology) on $X$. Therefore $\tau_{\mathcal B}$ is a topology on $X$.
[/step]
[step:Express every element of $\tau_{\mathcal B}$ as a union of basis elements]
Let $U \in \tau_{\mathcal B}$. For each $x \in U$, choose one basis element $B_x \in \mathcal B$ such that
\begin{align*}
x \in B_x \subset U.
\end{align*}
This choice is possible by the definition of $\tau_{\mathcal B}$. Define the indexed subcollection
\begin{align*}
\mathcal B_U := \{B_x \in \mathcal B : x \in U\}.
\end{align*}
Then
\begin{align*}
U = \bigcup_{x \in U} B_x.
\end{align*}
Indeed, if $y \in U$, then $y \in B_y \subset \bigcup_{x \in U} B_x$, so $U \subset \bigcup_{x \in U} B_x$. Conversely, for every $x \in U$ we have $B_x \subset U$, so $\bigcup_{x \in U} B_x \subset U$. Therefore every element of $\tau_{\mathcal B}$ is a union of elements of $\mathcal B$.
[/step]
