Definition: A net $\nu$ is said to be a subnet of net $\nu',$ if there exists some function $\varphi:\mathrm{dom}(\nu)\to \mathrm{dom}(\nu'),$ such that
$\bf 1)$ $\nu=\nu'\circ\varphi,$
$\bf 2)$ for each $n\in \mathrm{dom}(\nu'),$ there exists some $n'\in \mathrm{dom}(\nu),$ such that $d'\in \mathrm{dom}(\nu),\ d'\geqslant n'\Longrightarrow \varphi(d')\geqslant n.$
Suppose that we have a net $\nu,$ and there is a cardinal $\kappa$ satisfying $\kappa\geqslant \mathrm{Card}\big(\mathrm{dom}(\nu)\big)\geqslant \aleph_0.$
Question: Can we always find a net $\nu'$ such that $\mathrm{Card}\big(\mathrm{dom}(\nu')\big)=\kappa,$ and $\nu$ is a subnet of $\nu'?$
P.S. I encounter this problem when trying to find out the relationship between nets and sequences. If the answer is affirmative, then I could prove a very powerful theorem about the cardinal of nets.:)
Sure, you can always do this pretty trivially; roughly speaking, you just add irrelevant junk to the start of the net. Let $I=\mathrm{dom}(\nu)$ (with order $\leq_I$) and let $J$ be a set of cardinality $\kappa$ which contains $I$ as a subset. Pick any partial order $\leq_{J\setminus I}$ on the set $J\setminus I$ and let $${\leq_J}={\leq_{J\setminus I}}\cup{\leq_I}\cup (J\setminus I)\times I.$$ That is, we order $J$ by using $\leq_I$ on $I$, $\leq_{J\setminus I}$ on $J\setminus I$, and saying that every element of $J\setminus I$ is less than every element of $I$. It is easy to check that $\leq_J$ is a directed partial order.
Now let $\nu'$ be any extension of $\nu$ to a function defined on all of $J$ (just define it arbitrarily on $J\setminus I$). Then $\nu$ is a subnet of $\nu'$, via the inclusion map $I\to J$ (since every element of $I$ is greater than every element of $J\setminus I$).