Lie's third fundamental theorem

By [L1], identify $\mathfrak{g}$ with a Lie subalgebra of ${\mathfrak{g}\mathfrak{l}}_n(\mathbb{R})$. By [L2], it is the tangent algebra of a connected immersed Lie subgroup $H$ of ${\mathrm{GL}}_n(\mathbb{R})$. The intrinsic group $H$ is a finite-dimensional real Lie group even when its image is not closed.

Let $p:\tilde{H}\to H$ be the universal covering Lie group from [L3]. A covering homomorphism is a local diffeomorphism, so $d{p}_e$ is a Lie-algebra isomorphism. Hence $\mathrm{Lie}(\tilde{H})\cong \mathrm{Lie}(H)\cong \mathfrak{g}$, and $\tilde{H}$ is connected and simply connected. For $\mathfrak{g}=0$, this construction yields the one-point group.

Suppose $G_1$ and $G_2$ are connected simply connected integrations of $\mathfrak{g}$, and let $\alpha :\mathrm{Lie}(G_1)\to \mathrm{Lie}(G_2)$ be the Lie-algebra isomorphism induced by chosen identifications with $\mathfrak{g}$. By [L4], $\alpha$ and ${\alpha }^{-1}$ integrate uniquely to homomorphisms $F:G_1\to G_2$ and $Q:G_2\to G_1$. The differentials of $QF$ and $FQ$ are the identity maps, so uniqueness in [L4] makes these composites the identity homomorphisms. Thus $F$ is a Lie-group isomorphism. Countable choice enters only through [L2] and [L4]; Ado and the covering step add no stronger choice.