$X$ is compact iff every net in $X$ has a convergent subnet (using filters). I'm trying to prove that a topological space $X$ is compact iff every net has a convergent subnet.
Here is what I already know about compactness/filters:
A topological space $X$ is compact iff every filter on $X$ has an adherent point and I'd like to use the connection between filters and nets to prove this statement.
So, I attempted like this:
Let $X$ be compact and let $x:=(x_\alpha)_{\alpha\in I}$ be a net in $X$. Then we can associate a filter $\mathcal{F}_x$ to this net by
$$\mathcal{F}_x:= \operatorname{stack}\{\{x_n:n \geq m\}: m \in I\}$$
Because $X$ is compact, it follows that there is $y \in X$ such that $\mathcal{F}_x \dashv y$. We then know that $x = (x_\alpha)_{\alpha \in I} \dashv y$ as well (by one of the properties of this associated filter). Consequently, $x$ has a convergent subnet converging to $y$.
Conversely, let $\mathcal{F}$ be any filter on $X$. We can associate a net with this filter by considering the directed set 
$$I:= \{(x,F): x \in F, F \in \mathcal{F}\}$$
partially ordered via reverse inclusion, ignoring the first coordinate and the map 
$$N_\mathcal{F}: I \to X: (x,F) \mapsto x$$
then gives the desired net.
By assumption, this net has a convergent subnet, which after an analaguous reasoning tells us that $\mathcal{F}$ has an adherent point as well, showing that $X$ is compact.
Is this correct?
 A: a. A cluster point of the net $(x_a)_{a \in A}$ in $X$ is a $p$ such that for every (open) neighbourhood $O$ of $p$ and every $a \in A$ there is some $a' \ge a$ such that $x_{a'} \in O$. (The net is frequently in every neighbourhood of $p$). This is probably what you denote by $(x_a)_{a \in A} \dashv p$.
b. It is well-known (e.g. Willard, chapter 11) that $p$ is a cluster point of a net iff there is a subnet of that net that converges to $p$. You seem to assume this fact as known.
c. To a net we associate its tail filter (as Willard also does in chapter 12) and $p$ is a cluster point (or adherence point) of the tail filter iff $p$ is a cluster point of the original net. This is an easy exercise in definitions.
d. Similarly we can define a net $N_{\mathcal{F}}$ from a filter $\mathcal{F}$ as you do (Willard chapter 12 construction again) and note that $p$ is a cluster point of that $N_{\mathcal{F}}$ iff $p$ is a cluster point of $\mathcal{F}$, again an easy exercise in definitions.
So assuming you know


*

*$X$ is compact iff every filter on $X$ has a cluster point.


We can show the required


*$X$ is compact iff every net has a convergent subnet.


using these correspondences and facts: 
$2$, $\Rightarrow$: let $(x_a)_{a \in A}$ be a net in $X$ and $X$ compact. Its tail filter has a cluster point by "$1$, $\Rightarrow$" and that cluster point is also one for the net by c. Then b. tells us that $(x_a)_{a \in A}$ has a convergent subnet.
$2$, $\Leftarrow$: let $\mathcal{F}$ be a filter on $X$ (On $X$ we assume that every net has a convergent subnet), then $N_{\mathcal{F}}$ has a convergent subnet to some $p$. So by b. (reverse direction) $p$ is a cluster point of $N_{\mathcal{F}}$ and so by d. $p$ is a cluster point of $\mathcal{F}$. Then $1$,$\Leftarrow$ tells us that $X$ is compact (as the filter was arbitrary).
So your argument is in essence correct. I just made all the known facts more explicit. So if a-d are all known to you you can use the final proof; maybe you need more details filled in for d? You seem to skip over some details there. 
A: A direct proof, not using the correspondences is also quite doable:
Suppose $X$ is compact, and $(x_a)_{a \in A}$ is any net. We only need to show that $p$ has a cluster point to get a convergent subnet. So suppose no point is a cluster point, and so we can pick for every $x \in X$ some open neighbourhood $U_x$ such that $$\exists a(x) \in A: \forall a \ge a(x): x_a \notin U_x\tag{1}$$
This defines an open cover of $X$ that has a finite subcover $\{U_x: x \in F\}$ for some finite subset $F$ of $X$. Now by directedness (applied finitely many times) we can find $a_0 \in A$ such that $\forall x \in F: a_0 \ge a(x)$. Now $p=x_{a_0}$ must lie in some $U_x$ for $x \in F$, but then $a_0 \ge a(x)$ directly contradicts $(1)$, as we have $p \in U_x$ and simultaneously $p \notin U_x$. This contradiction shows that the net does have a cluster point and we're done.
So suppose every net has a cluster point (or equivalently, a convergent subnet) and we'll show $X$ is compact: let $\mathcal{U}$ be an open cover of $X$ and suppose it has no finite subcover (going for a contradiction). Define a directed set by $$I = \{(\mathcal{U}', x): x \in X \setminus \bigcup \mathcal{U}', \mathcal{U}' \subseteq \mathcal{U} \text{ finite }\}$$ ordered by inclusion on the first component and a net $n:I \to X$ by $n(\mathcal{U}', x)= x$. This definition only works because the cover has no finite subcovers.
Then if $x \in X$, let $U_x \in \mathcal{U}$ so that $x \in U_x$, then pick any $y \notin U_x$ (otherwise $U_x=X$ and $\mathcal{U}$ would have had a finite subcover) and define $i(x)=(\{U_x\},y)$ and by definition if $i \ge i_0$, $n(i) \notin U_x$, so the pair $U_x$ and $i_0$ witness that $x$ is not a cluster point of $n$. So as $x$ was arbitrary, the net $n$ has no cluster points and we have our contradiction. So $X$ is compact.
