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.
It is far easier to first characterize open sets in terms of nets as follow
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.