Every net has an ultranet as subnet: direct proof

I'm currently brushing up my topology using Willard's General Topology. Currently I'm working through the chapters 11 and 12 on nets and filters. Chapter 12 deals extensively with ultrafilters and proves (Theorem 12.12) that every filter is contained in an ultrafilter using Zorn's lemma.

Theorem 12.17 and the exercises connect nets and filters. In this way, I see a proof that:

Every net has a subnet which is an ultranet.

For reference:

A subnet $x_\mu$ of $x_\lambda$ is an increasing cofinal mapping $\phi: M\to\Lambda$ composed with $x: \Lambda\to X$.

An ultranet is a net $x: \Lambda \to X$ such that: $$\forall E \subseteq X: \exists \lambda_0: \forall \lambda\ge \lambda_0: x_\lambda \in E \lor \forall \lambda\ge \lambda_0: x_\lambda\notin E$$

However, this very statement also occurs as Exercise 11B.2. This suggests an easier proof. After one and a half week of intermittent attempts, I concede and humbly ask your help.

I would love to see "natural proofs", as opposed to deus ex machina constructions. Thanks in advance. (It should be noted that some choice is necessary, but even in choice proofs, some are more natural than others.)

Solution 1:

Let $f: I \to X$ be net in $X$, where $(I, \le)$ is a directed set. To build a universal subnet: let $\mathcal{F}$ be the filter of tails on $X$, so the filter generated by all $T(i) = \{f(j): j \ge i\}, i \in I$, cf. definition 12.15 in Willard, and (the non-constructive part) let $\mathcal{U}$ be an ultrafilter on $X$ extending $\mathcal{F}$. Then let $J = \{(i, U) \in I \times \mathcal{U}: f(i) \in U \}$ be a set with order $(i, U_1) \le (i' ,U_2)$ iff $i \le i'$ and $U_2 \subseteq U_1$, which is clearly a directed set. Define a net $g: J \to X$ by $g(j) = g((i,U)) = x_i$. This is a subnet of $f$ (use the projection as the connecting map). One only has to show that $g$ is indeed a universal net.

If you get stuck on that part my note here might help...

All published proofs that I know of the existence of ultranets use ultrafilters or ultrafilters in disguise (as a maximal of family of subsets of certain type). I think this has to do with the fact that there is no set of subnets of a given net; as the index set of a subnet can be any directed set, the collection of subnets form a proper class in general, and so we cannot easily apply maximum principles like Zorn’s lemma.