size issue related to universal quantifications over nets

Question

In this wikipedia article, it is written that

A function $f : X \rightarrow Y$ between topological spaces is continuous at the point $x$ if and only if for every net $(x_\alpha)$ with $\lim x_\alpha = x$ we have $\lim f(x_\alpha) = f(x)$ .

I'm wondering if there is a size issue related to the phrase "for every net".

A net is a function from a directed set to a set, so I think that we need the set of all sets to construct the set of all directed sets and do universal quantifications over it.

Answer 1

No, the statement is just "for every set $A$ that is directed and for every net $A\to X$..." This is a statement in first order logic that quantifies over all sets and is precisely the kind of thing we are allowed to do in ZF. Where size issues come in is when we try to quantify over all collections of sets (i.e. classes).$^*$

Not sure if this will make you feel better or worse at this point, but consider the power set of a set $X.$ It is the collection of all sets that are subsets of $X$ (which is a set provided we have the power set axiom). Notice we quantified over all sets in this definition too.

---

$^*$ There are usually a lot of questions at this point, like (1) "Aren't sets collections of sets?" and (2) "What does 'all sets' mean?" I'm pretty sure there's plenty of material on these kinds of questions on this site and overflow, so I'll only answer very briefly.

1. Sets have extensions, which are collections of sets related to them by the membership relation. Some collections are the extension of a set and others, e.g. the collection of all sets, are not. Colloquially, "the class is a set". Paradoxes are avoided by only allowing strong enough axioms to prove certain classes are sets. ZFC is strong enough to be very expressive while still weak enough to avoid all known possible contradictions.
2. We just assume there is some universe of sets that obeys the ZFC axioms, and that is where set-theoretically founded mathematics takes place (when and if we care about foundations and decide to use set theory). We can't really construct one in a satisfying way, since ZFC is powerful enough to do pretty much any construction that would be commonly accepted, and construction of a model of ZFC can't be done in ZFC due to the incompleteness theorem.

Answer 2

When we quantify as "for all $x$ in $T$ ...", $T$ is a type and need not be a set.

So we can quantify on the type of all sets like $\forall x \in \text{Set}(\varphi(x))$, without constructing the set of all sets.