Uniformization of simply connected Riemann surfaces

Setup and the dichotomy at the chosen pole. The surface $X$ is nonempty [F1], so fix a point $p_0\in X$; by [F2] the envelope $g_X(\cdot ,p_0)$ is defined on $X\setminus \{p_0\}$ with values in $[0,+\mathrm{\infty }]$. Since the Axiom of Choice [A1] supplies the Countable Choice required by [F3], the dichotomy applies to the pole $p_0$: either $g_X(q,p_0)=+\mathrm{\infty }$ for every $q\in X\setminus \{p_0\}$, or $g_X(\cdot ,p_0)$ is finite on $X\setminus \{p_0\}$, which by [F2] says exactly that $X$ admits a finite canonical Green kernel at $p_0$.

Finite case: $X$ is the disc. If $X$ admits a finite canonical Green kernel at $p_0$, then the Green case [F4] applies to the simply connected surface $X$ and provides a biholomorphism of $X$ onto the unit disc $\mathbb{D}$.

Infinite case: $X$ is the plane or the sphere. If instead $g_X(q,p_0)=+\mathrm{\infty }$ for every $q\in X\setminus \{p_0\}$, then the non-Green case [F5] applies: $X$ is biholomorphic to $\mathbb{C}$ when $X$ is noncompact, and to $\widehat{\mathbb{C}}$ when $X$ is compact.

Every simply connected surface is one of the three models. The two alternatives of step 1.1 exhaust the possibilities for the envelope $g_X(\cdot ,p_0)$ by the dichotomy [F3]; hence steps 2.1 and 2.2 show that $X$ is biholomorphic to $\mathbb{D}$, to $\mathbb{C}$ or to $\widehat{\mathbb{C}}$. Moreover the last two are themselves simply connected Riemann surfaces [F6], so each alternative really is one of the three models.

At most one model. Suppose that $X$ is biholomorphic to two of the models, say to $M_1$ and to $M_2$ with $M_1,M_2\in \{\widehat{\mathbb{C}},\mathbb{C},\mathbb{D}\}$; then $M_1$ is biholomorphic to $M_2$, because the composite of a biholomorphism $X\to M_1$ with the inverse of a biholomorphism $X\to M_2$ is again a biholomorphism [F1]. By [F6] no two distinct members of $\{\widehat{\mathbb{C}},\mathbb{C},\mathbb{D}\}$ are biholomorphic, so $M_1=M_2$. Hence $X$ is biholomorphic to at most one of the three models.

Conclusion and choice accounting. Steps 3.1 and 4.1 together say that $X$ is biholomorphic to exactly one of the Riemann sphere, the complex plane and the unit disc, which is the statement. The Axiom of Choice [A1] is used exactly through the Countable Choice consumed by the dichotomy [F3] in step 1.1 and through its two uses in the branch lemmas, namely the Riemann mapping theorem inside [F4] and [F5]; beyond the single point $p_0$ chosen in step 1.1 no selection is made.