A problem in my book states to prove where is a positive integer.

This problem requires to construct a one-to-one mapping from .

I think I found a way to do this using transfinite recursion however it is not explicit. Is that good enough? Because recursion is not actually explicit. Is there an actual way of constructing an explicit correspondence from to ? My intuition begins to break down when dealing with very large sets.

Here is how I was doing it. This is the following transfinite recusion theorem I will use: let be an ordinal and a set, given there exists (a unique) function so that for all .

We begin by well-ordering lexiographically. Let . Let . Now define a function as . By transfinite recursion there exists a function so that .

To complete the proof that provides a bijection we need to do show a few more details. One of them is that must attain a value of at some point. Because otherwise we would have an injection from , and arrive at a contradiction from there.

I just do not like this approach because it is not really an explicit mapping.