Showing that a mapping $f:X \to Y$ is continuous at $z_0 \in X$ when the net $f \circ \varphi$ converges to $f(z_0)$ with $\varphi\to z_0$ Let $(X, \tau_1), (Y, \tau_2)$ be topological spaces, $f:X\to Y$ a mapping, $\varphi:S\to X$ a net converging to $z_0$ and suppose that the composition $f \circ \varphi$ converges to $f(z_0)$. Here $S$ is a directed set equipped with the direction relation $\leq$ s.t. for all $a, b, c \in S: a \leq a\land a\leq b\leq c \implies a \leq c$ and if $a, b \in S$ then there exists $d \in S: a \leq d \land b \leq d$.
The convergence of $\varphi$ to $z_0$ means that for any neighborhood $N$ of $z_0$ there exists $\gamma \in S$ such that for all $a \in S: a\geq \gamma: \varphi(a) \in N$. Below (and in the title) I'm using $\to$ to indicate convergence to as in regular analysis.
I'm trying to show that $f$ is continuous at $z_0$, i.e. for any neighborhood $N_2$ of $f(z_0)$ there exists a neighborhood $N_1$ of $z_0$ s.t. $f[N_1] \subset N_2$. So far what I've managed to argue is that if $N_1$ and $N_2$ are any two neighborhoods of $z_0$ and $f(z_0)$, respectively, then as $f \circ \varphi \to f(z_0)$ and $\varphi\to z_0$, there exists $\gamma_1, \gamma_2 \in S$ such that for all 1.)  $a \in S:a\geq \gamma_1:\varphi(a) \in N_1 \implies f(\varphi(a)) \in f[N_1]$ and 2.) $a \in S:a\geq \gamma_2:(f\circ \varphi)(a) \in N_2$. Then I've used the properties of the direction relation to take $\gamma' \geq \gamma_1, \gamma'\geq \gamma_2$ to unify the quantifiers for both of the expressions. But the issue with the current work is that now I've only shown that $N_2 \cap f[N_1]\neq \varnothing$, while I would need to show that $f[N_1] \subset N_2$. And as of now it is not clear to me how to establish the relationship between the neighborhoods of $z_0$ and $f(z_0)$ with the properties of the net.
 A: It is far easier to first characterize open sets in terms of nets as follow

Lemma: a set $U \subset X$ is open if and only if for all net $\varphi: S \to X$ converging to $x \in U$, there exists $s \in S$
such that for all $t \in S,\  t > s \implies \varphi(t) \in U$.
Proof: the set $U$ is open if and only if for all $x \in U$, there exists a neighbourhood of $x$ in $U$. The if direction is easy. Let's assume that $U$ is open and $\varphi : S \to X$ is a net converging to $x \in U$. Since $U$ is open, $U$ is a neighbourhood of $x$. So by definition of the convergence of nets, there exists $s \in S$ such that $\forall t \in S,\ t> s \implies \varphi(t) \in U$.
Let us prove the opposite direction. Fix $x \in U$ and assume there is no such a neighbourhood. Let S denotes the set of neighbourhoods of $x$. The relation $N_1 \leqslant N_2$ with $N_1, N_2 \in S$ is defined by $N_2 \subset N_1$. It is clear that $(S, \leqslant)$ is a directed set. By assumption, for any $N \in S$, there exists $y \in N \cap (X-U)$. By the axiom of choice, there exists $\varphi: S \to X$ such that $\varphi(N) \in N \cap (X-U)$. Thus $\varphi$ is a net converging to $x$ but for any $N \in S$, $\varphi(N) \not \in U$. That is a contradiction.

The above lemma cannot be proved in ZF only. See the section 4.6 of Axiom of Choice by Herrlich. In some models of ZF, there exists a sequentially continuous function $f : \mathbb{R} \to \mathbb{R}$ which is not continuous.
Now, we can prove the characterization of continuous functions in terms of nets.
Pick $U$ an open subset of $Y$. We have to show that $f^{-1}(U)$ is open in $X$. Let $\varphi : S \to X$ be a net converging to $x \in f^{-1}(U)$. By hypothesis, we know that $f \circ \varphi$ is a net converging to $f(x)$ and $f(x) \in U$. But $U$ is open, thus there exists a rank $s \in S$ such that $\forall t \in S,\ t > s \implies (f \circ \varphi)(t) \in U$. We deduce that $\forall t \in S$, $t > s \implies \varphi(t) \in f^{-1}(U)$. So $f^{-1}(U)$ is open and $f$ is continuous.
