Synopsis
In my studying of Set Theory, I've had the privilege of being able to compare much of my work to a solutions manual. This solutions manual, however, ended after the chapter on the various number systems. As such, I'm going to start posting a lot of my own personal solutions or questions onto the site for either proof validation or proof hints (if I'm unable to find the solution in other places), and I would greatly appreciate any feedback on my mathematical writing. Thank you.
Exercise
Show that the equation $$f(m, n) = 2^m(2n + 1) - 1$$ defines a one-to-one correspondence between $\omega \times \omega$ and $\omega$.
Proof
First, we show that $f$ is injective. Consider $(m, n)$ and $(m', n')$ in $\omega \times \omega$. Now suppose that $f(m, n) = f(m', n')$. Then $2^{m}(2n+1) - 1 = 2^{m'}(2n' + 1) - 1$ and $2^{m}(2n+1) = 2^{m'}(2n' + 1)$. Note that every value of this equation will only have one odd factor, mainly $(2n + 1)$. As such, $n = n'$ and $2^m = 2^{m'}$. So, $m = m'$ and $f$ is injective.
Next, we wish to show that $f$ is surjective. Consider any $x \in \omega$. If $x$ is even, take $m = 0$ and $n = x/2$. If $x$ is odd, note that $x = 2k + 1$ for some $k \in \omega$. So $2k = 2^m(2n + 1)$ if $m$ and $n$ exist, and since every even number contains a factor that is odd (for powers of two, we consider the factor one), there is always a $m$ and $n$ that satisfies the equality. Therefore, for any $x \in \omega$, there is always a $m$ and $n$ such that $f(m, n) = 2^m(2n + 1) - 1$ and $f$ is surjective.
As such, because $f$ is both surjective and injective, $f$ is bijective, and the equation $f(m, n) = 2^m(2n + 1) - 1$ defines a one-to-one correspondence between $\omega \times \omega$ and $\omega$.
Proof looks fine.
For the $x$ odd case, you might want to clarify whether when using $n=0$ for the "odd factor one" interferes with $k$ itself being odd (hence $m=1$).
It might be easier to simply write down $m$ and $n$ in terms of the factorization of $k$ (at least for prime $2$ and everything else).
This tracks closer to why this entire construction works: you're essentially splitting up all natural numbers into the direct product of two copies of itself, one half encoded by powers of 2, the other half by all odd numbers. Fundamental theorem of arithmetic makes this work both ways (per Anonymous).