An explicit enumeration of the rationals, with repetitions and then without them

$J$ is a bijection $\mathbb{N}\times \mathbb{N}\to \mathbb{N}$: by [F1], $J={\sigma }^{-1}\circ J_0$ is a composite of the bijection $J_0$ with the bijection ${\sigma }^{-1}$, and $2^m(2n+1)-1$ is exactly its value, $-1$ being the value of ${\sigma }^{-1}$ on $\mathbb{N}\setminus \{0\}$. Hence for every $n\in \mathbb{N}$ the pair $J^{-1}(n)$ is defined and unique, and same for iterated decoding.

The map $q$ is a well-defined function $\mathbb{N}\to \mathbb{Q}$ with the displayed rule. For $n\in \mathbb{N}$, step 1.1 gives unique $u,c\in \mathbb{N}$ with $J(u,c)=n$, then unique $a,b$ with $J(a,b)=u$, so $z(u):=[(a,b)]$ is a well-defined integer by [F2]. Since $c+1=\sigma (c)\mathrm{\ne }0$ by [F1] and the embedding $k\mapsto \bar{k}$ is injective, $\overline{c+1}$ is a nonzero integer, so $(z(u),\overline{c+1})$ is a legitimate pair of integers with nonzero second component and $q(n):=[(z(u),\overline{c+1})]$ is a rational, the class being formed by The rationals as equivalence classes of pairs of integers; all clauses are given by formulas, so $q$ is a function.

The first values: $J^{-1}(0)=(0,0)$ because $J(0,0)=2^0\cdot 1-1=0$, so $q(0)=[(z(0),\bar{1})]$ where $z(0)=[(0,0)]=0$ and $\bar{1}=1$, giving $q(0)=0$. Next $J(1,0)=2-1=1$, so $J^{-1}(1)=(1,0)$ and $z(1)=[(1,0)]=1$, giving $q(1)=[(1,1)]=1$. Next $J(0,1)=3-1=2$, so $J^{-1}(2)=(0,1)$, $z(0)=0$ and $q(2)=[(0,\bar{2})]=0$. Next $J(2,0)=4-1=3$, so $J^{-1}(3)=(2,0)$, and $J^{-1}(2)=(0,1)$ gives $z(2)=[(0,1)]=-1$, so $q(3)=[(-1,\bar{1})]=-1$.

$q$ is surjective. Let $x\in \mathbb{Q}$. By [F4] fix a representative $(p,v)$ of $x$ with $v>0$; by [F2] write $p=[(a,b)]$ with $a,b\in \mathbb{N}$; by [F3] write $v=\bar{k}$ with $k\in \mathbb{N}$, and $k\mathrm{\ne }0$ because $v>0=\bar{0}$ and $k\mapsto \bar{k}$ preserves order. Then $k=\sigma (c)$ for some $c\in \mathbb{N}$ (Every nonzero natural number is a successor), so $c+1=k$. Put $u:=J(a,b)$ and $n:=J(u,c)$; then $J^{-1}(n)=(u,c)$ and $J^{-1}(u)=(a,b)$, so $z(u)=[(a,b)]=p$ and $q(n)=[(p,\overline{c+1})]=[(p,v)]=x$. Hence every rational is a value of $q$.

Let $M:=\{n\in \mathbb{N}:\text{for all }k<n,q(k)\mathrm{\ne }q(n)\}$, the set of first occurrences of values of $q$, a subset of $\mathbb{N}$ by Separation. Then $M$ is infinite. Indeed, by [F5] the map $f(i):=[(\bar{i},1)]$ is an injection $\mathbb{N}\to \mathbb{Q}$; for each $i$ the set $A_i:=\{n\in \mathbb{N}:q(n)=f(i)\}$ is nonempty by step 3.1 and has a least element $m_i$ by [F6]. Each $m_i$ lies in $M$, since for $k<m_i$ minimality gives $q(k)\mathrm{\ne }f(i)=q(m_i)$; and $i\mapsto m_i$ is injective because $f$ is. An injection $\mathbb{N}\to M$ rules out $M\approx t$ for any $t\in \mathbb{N}$: composing it with a bijection $M\to t$ would be an injection $\mathbb{N}\to t$, whose restriction to $\sigma (t)$ would be an injection $\sigma (t)\to t$, which [F6] forbids.

$M$ is unbounded in $\mathbb{N}$. If $M$ were bounded above by some $b\in \mathbb{N}$, then $M\subseteq \sigma (b)$ by [F7] and $M$ would be finite by [F7], contradicting step 4.1.

By step 5.1 and [F7] there is an increasing bijection $e:\mathbb{N}\to M$: it is the increasing enumeration of the unbounded set $M$, with $e(i)<e(j)$ whenever $i<j$.

The composite $j\mapsto q(e(j))$ is injective. If $i<j$ then $e(i)<e(j)$ by step 6.1, and $e(j)\in M$ means $q(k)\mathrm{\ne }q(e(j))$ for every $k<e(j)$; taking $k=e(i)$ gives $q(e(i))\mathrm{\ne }q(e(j))$.

The composite $j\mapsto q(e(j))$ is surjective. Let $x\in \mathbb{Q}$; by step 3.1 there is $n$ with $q(n)=x$, and $k:=\min \{n:q(n)=x\}$ exists by [F6]. Then $k\in M$, because any $k^{\mathrm{\prime }}<k$ has $q(k^{\mathrm{\prime }})\mathrm{\ne }x=q(k)$ by minimality, and $e$ is onto $M$ by step 6.1, so $k=e(j)$ for some $j$ and $x=q(k)=q(e(j))$.

Therefore $j\mapsto q(e(j))$ is a bijection $\mathbb{N}\to \mathbb{Q}$ by steps 7.1 and 7.2, so $\mathbb{Q}\approx \mathbb{N}$ and $\mathbb{Q}$ is countably infinite by [F8]. Every object was built by an explicit formula — the pairing $J$, the decoded pairs, the classes, the least elements and the increasing enumeration of $M$ — so no choice principle is used.