$3$ equivalent definitions of compactness I'm trying to prove this equivalence. Could you have a check on my attempt?

Let $X$ be a topological space. The following statements are equivalent.

*

*(S1) Every open cover of $X$ has a finite subcover.

*(S2) Every net in $X$ has a convergent subnet.

*(S3) Any collection of closed subsets of $X$ with the finite intersection property has nonempty intersection.


My proof:

*

*S1 $\implies$ S2

Assume the contrary that there is a net $(x_d)_{d\in D}$ that does not have any convergent subnet. This implies $(x_d)_{d\in D}$ does not have any cluster point. This means for every $x \in X$, there exist a neighborhood $U_x$ of $x$ and $d_x \in D$ such that for all $d \ge d_x$, $x_{d} \notin U_x$. WLOG, we assume $U_x$ is open for all $x\in X$.
Clearly, $(U_x)_{x\in X}$ is an open cover of $X$. So there is a finite set $I \subseteq X$ such that $(U_x)_{x\in I}$ covers $X$. Let $d^* := \max \{d_x \mid x \in I\}$. Because $I$ is finite, $d^*$ is well-defined. Hence $x_d \notin \bigcup_{x\in I} U_x = X$ for all $d \ge d^*$. This is a contradiction.

*

*S2 $\implies$ S3

Let $(A_i)_{i\in I}$ be a family of closed subsets of $X$ with the finite intersection property. Let $\mathcal J$ be the set of non-empty finite subsets of $I$. We define a pre-order $\le$ on $\mathcal J$ by $J_1 \le J_2 \iff J_1 \subseteq J_2$. Then $\mathcal J$ together with $\le$ is a directed set. By axiom of choice, there is $x_J \in \bigcap_{i\in J} A_i$ for all $J \in \mathcal J$. Then $(x_J)_{J \in \mathcal J}$ is a net in $X$. Then it has a convergent subnet $(x_{\varphi(d)})_{d\in D}$, i.e., $x_{\varphi(d)} \to x$ for some $x\in X$.
We claim that $x \in \bigcap_{i \in I} A_i$. If not, there is $i_0 \in I$ such that $x \notin A_{i_0}$. Then there is a neighborhood $U_{0}$ of $x$ such that $U_{0} \subseteq A_{i_0}^c$. On the other hand, there is some $d_0 \in D$ such that $x_{\varphi(d)} \in U_0$ for all $d \ge d_0$. Because $\varphi$ is cofinal in $\mathcal J$, there is $d'\in D$ such that $\varphi(d') \ge \varphi(d_0) \cup \{i_0\}$. Also, there is $d^*\in D$ such that $d^*\ge d_0$ and $d^* \ge d'$ This means $x_{\varphi(d^*)} \in U_0$ and $x_{\varphi(d^*)} \in A_0$, so $U_0 \cap A_0 \neq \emptyset$, which is a contradiction.
Remark: We can obtain $x \in \bigcap_{i \in I} A_i$ in more elegant way. We have $x_{\varphi(d)} \to x$ implies for each neighborhood $U$ of $x$, there is $d_U \in D$ such that $x_{\varphi(d)} \in U$ for all $d \ge d_U$. This means $U \cap A_i \neq \emptyset$ and thus  $x \in \overline{A_i} = A_i$ for all $i\in I$.

*

*S3 $\implies$ S1

Let $(A_i)_{i\in I}$ be an open cover of $X$ and $B_i := A_i^c$. If $(A_i)_{i\in I}$ does not have an finite subcover, then $(B_i)_{i\in I}$ is collection of closed subsets of $X$ with the finite intersection property. This means $\bigcap_{i\in I} B_i \neq \emptyset$ and thus $\left (\bigcup_{i\in I} A_i \right)^c \neq \emptyset$, which is a contradiction.
 A: The S1 $\implies$ S2 proof is mostly fine: I'd also use the cluster point / convergent subnet approach and choose said $d_x$.
But a flaw is to define $d^\ast* = \max\{d_x\mid x \in I\}$: in a directed set we do not have a maximum, even for two elements (that would say all such sets are linearly ordered, and one of the points of nets is that they need not be); we only know that by definition
$$\forall d_1,d_2 \in D: \exists d_3 \in D: (d_1 \le d_3) \land (d_2 \le d_3)\tag{1}$$
i.e. each pair of elements has a common upperbound, or $\{d_1,d_2\}$ has an upperbound in $D$. Then by a simple induction (on cardinality) it follows that for any finite subset $F \subseteq D$ there is an upperbound for $F$ in $D$, so
$$\exists d_F^\ast \in D: \forall d \in F: d \le d_F^\ast$$
and this last fact can be applied to your $\{d_x: x \in I\}$, salvaging the proof. Beware of this subtlety!
In S2 $\implies$ S3 the proof could be smoother if in your proof your just say directly that $(x_J)_{J \in \mathcal{J}}$ has a cluster point $p \in X$ (which is implied by having a convergent subnet; if I can I try to avoid subnet arguments in favour of cluster point ones: it avoids discussion about what type of subnet we're dealing with etc.)
Then $p \in \bigcap_{i \in I} A_i$ is not hard: fix $i \in I$ for now. Let $U $ be any open neighbourhood of $p$. Then $\{i\} \in \mathcal{J}$ so by being a cluster point, for some $J \in \mathcal{J}$ with $\{i\} \le J$ we have $x_J \in U$. But then $i \in J$ and $x_J \in \bigcap_{j \in J} A_j \subseteq A_i$ and so $U \cap A_i \neq \emptyset$. As $U$ was arbitary, $p \in \overline{A_i}=A_i$ and as $i$ was arbitrary, we're done.
Another way is to bypass the index set altogether: if $\mathcal{F}$ is a family of closed sets with FIP, add all finite intersections from $\mathcal{F}$ too and we create a family $\mathcal{F}'$ of closed sets containing $\mathcal F$ which is closed under finite intersections and obeys $\bigcap \mathcal F = \bigcap \mathcal F'$ so it suffices to show the latter intersection to be non-empty. Then define a direction $\le'$ on $\mathcal F'$ by $F \le G \iff G \subseteq F$ (reversing the inclusion like in defining nets using the neighbourhood filter) and this is well-defined as $\mathcal F'$ is closed under finite intersections by construction. Again for each $F \in \mathcal F'$ we pick by AC some $x_F \in F$ to define a net. We get a cluster point $p$ of this net as before and then if $F \in \mathcal{F}$  and $U$ an open neighbourhood of $p$ we have some $G \in \mathcal F'$ so that $F \le' G$ and $x_G \in A$ and then $x_G \in G \subseteq F$ immediately implies $A \cap F \neq \emptyset$ etc.
It's the same proof in a different (maybe nicer?) guise. Making families closed under convenient operations is a common proof idea. I quite like to use it.
I have nothing to add for S3 $\implies$ S1, except maybe: add the short proof that FIP-ness of the $U_i^\complement$ family is equivalent to the fact that no finite subfamily of the $U_i$ can cover $X$. Being precise is a good thing. It's all just de Morgan's laws anyway.
Good job overall, modulo the subtlety..
