Neighbourhood filter of a uniform space The Wikipedia page for Uniform space includes the following section: 

Every uniform space $V$ becomes a topological space by defining a subset $O$ of $X$ to be open if and only if for every $x$ in $O$ there exists an entourage $V$ such that $V[x]$ is a subset of $O$. In this topology, the neighbourhood filter of a point $x$ is $\{V[x] : V∈Φ\}$. This can be proved with a recursive use of the existence of a "half-size" entourage. Compared to a general topological space the existence of the uniform structure makes possible the comparison of sizes of neighbourhoods: $V[x]$ and $V[y]$ are considered to be of the "same size".

While I have worked through and proved that the topology described is in fact a topology, I'm stuck on how it can be proved that $\{V[x] : V∈Φ\}$ defines the neighbourhood filter of $x$, as I don't understand what the hint there is trying to tell me. 
I want to work through the full proof myself, but are there any extra hints to push me in the right direction? 
 A: Let $(X,\mathcal{U})$ be a uniform space, defined in terms of
entourages, following the axioms as described in Wikipedia.
First check that $\mathcal{B}_x:= \{V[x]: V \in \mathcal{U}\}$ (which is
non-empty, as $\mathcal{U}$ is non-empty) is a filter base (closed under
finite intersections even):


*

*$x \in V[x]$ for every $V \in \mathcal{U}$, as $(x,x) \in \Delta
\subseteq V$. So all $V[x]$ are non-empty. 

*If $V[x], W[x]$ are in
$\mathcal{B}_x$, so $V,W \in \mathcal{U}$, then  $U = V \cap W\in
\mathcal{U}$. Then $U[x] = V[x] \cap W[x]$, which follows from the
definitions: $y \in U[x]$ iff $(x,y) \in U$ iff $(x,y) \in V$ and $(x,y)
\in W$ iff $y \in V[x]$ and $y \in W[x]$ iff $y \in V[x] \cap W[x]$.


The claim on the page should be that the generated filter
$$\mathcal{U}_x = \{O \subseteq X \mid \exists U \in \mathcal{U}: U[x]
\subseteq O\}$$
is the neighbourhood filter of the topology
$$\mathcal{T} = \{O \subseteq X \mid \forall x \in O: O \in
\mathcal{U}_x\}$$
This $\mathcal{T}$ is the topology induced by the uniformity.
Let's check first that this actually defines a topology:


*

*$\emptyset \in \mathcal{T}$ because a $\forall x \in O$ formula always
holds for $O = \emptyset$, it's vacuously true. $X \in \mathcal{T}$
because for every $x \in X$, $X \in \mathcal{U_x}$ because $X$ is a
superset of any member of $\mathcal{B}_x$ (which as said is non-empty).

*If $O_1, O_2 \in \mathcal{T}$, it suffices to show that $O_1 \cap O_2
\in \mathcal{T}$: let $x \in O_1 \cap O_2$. As $O_1$ is open, $O_1 \in
\mathcal{U_x}$. Also, because $O_2$ is open, $O_2 \in \mathcal{U}_x$.
This in turn means we have $U \in \mathcal{U}$ with $U[x] \subseteq O_1$
and $V \in \mathcal{U}$ such that $V[x] \subseteq O_2$. We saw at the
top that $(U \cap V)[x] = U[x] \cap V[x] \subseteq O_1 \cap O_2$, and as
$U \cap V \in \mathcal{U}$ we see that $O_1 \cap O_2 \in \mathcal{U}_x$.
As this holds for all $x \in O_1 \cap O_2$, $O_1 \cap O_2 \in
\mathcal{T}$. 

*If $O_i \in \mathcal{T}$, for $i \in I$, then $O =
\bigcup_i O_i \in \mathcal{T}$: let $x \in O$. Then for some $i_0 \in
I$, $x \in O_{i_0}$, and as the latter set is open, we know that $O_{i_0}
\in \mathcal{U}_x$, and so, as $O_{i_0} \subseteq O$,
so also $O \in \mathcal{U}_x$, and as $x \in O$ was arbitrary, $O \in
\mathcal{T}$ as required.


So far, we've used very little of the axioms for a uniformity. To see
that $\mathcal{B}_x$ is actually a local base at $x$ for $\mathcal{T}$, we need a small 
lemma, that will use the missing axioms later on:

If $U \in \mathcal{U}$ be symmetrical and suppose $V$ is an entourage such that 
  $V \circ V \subseteq U$, we have that 
  $$\forall y \in V[x] : V[y] \subseteq U[x]$$

Proof: take $y \in V[x]$ and to see the inclusion pick $z \in V[y]$. We have $(x,y) \in V$
and $(y,z) \in V$ so $(x,z) \in V \circ V \subseteq U$, so $(x,z) \in U$ by symmetry,
and hence $z \in U[x]$; this shows $V[y] \subseteq U[x]$.
This lemma provides a link between neighbourhood systems of different points, while
so far everything has been very "pointwise".
Then let $\mathcal{N}_x$ be the neighbourhood filter of $x$ as determined by the topology $\mathcal{T}$: i.e.
$$\mathcal{N}_x = \{N: \exists O \in \mathcal{T}: x \in O \subseteq N\}$$
We want to show that $\mathcal{N}_x = \mathcal{U}_x$ for all $x$.
This would show that the $\mathcal{B}_x = \{U[x]: U \in \mathcal{U}\}$ form a base of neighbourhoods for $\mathcal{T}$ at $x$,
which is what we wanted to show.
Left to right inclusion:
Suppose $N \in \mathcal{N}_x$ so there is $x \in O \subseteq N$. As $O$ is open and $x \in O$ we
have that $O \in \mathcal{U}_x$, and so $N \in \mathcal{U}_x$ as this is a filter. Pretty much by construction.
Right to left:
Let $N \in \mathcal{U}_x$.
Define:
$$O = \{p \in X: N \in \mathcal{U}_p\}$$
Then by definition $x \in O$. Also, $O \subseteq N$ is clear ($y \in O \implies N \in \mathcal{B}_y$ 
and as all members of $\mathcal{B}_y$ contain $y$, $y \in N$ as well).
Let $y \in O$, so that $N \in \mathcal{U}_y$. This says that there is some $U \in \mathcal{U}$
such that $U[y] \subseteq N$. WLOG we can choose $U$ to be symmetrical, otherwise we replace it by 
$U \cap U^{-1} \in \mathcal{U}$, which is symmetrical. (by axioms 3,5). By axiom 4 we then find 
$V \in \mathcal{U}$ such that $V \circ V \subseteq U$.
We then have for all $z \in V[y]$ that $V[z] \subseteq U[y] \subseteq N$, so $N \in \mathcal{U}_z$ 
for all $z \in V[y]$. Hence $V[y] \subseteq O$ by definition of the set $O$.
So in summary 
$$\forall y \in O: \exists V \in \mathcal{U}: V[y] \subseteq O$$ 
This implies that (by the definition of $\mathcal{U}_x$):
$$\forall y \in O:  O \in \mathcal{U}_y$$
So $O \in \mathcal{T}$ and hence is open. So we have found $O$ open such that $x \in O \subseteq N$, so $N \in \mathcal{N}_x$.
This concludes the proof of the inclusion. 

We only need one invocation of axiom 4 (the "halving axiom") so I don't quite understand the remark about recursive use of this axiom that you mentioned.
