Connected covers of smooth manifolds have a canonical smooth structure

If $E=\mathrm{\varnothing }$, surjectivity in the covering-map definition forces $M=\mathrm{\varnothing }$; the empty pulled-back atlas gives the unique compatible smooth structure, the local-diffeomorphism condition is vacuous, and the asserted dimension is the supplied dimension $n$ of $M$. Henceforth assume $E\mathrm{\ne }\mathrm{\varnothing }$. The space $E$ is locally Euclidean of dimension $n$: if $U\subseteq M$ is an evenly covered coordinate domain and $S$ is a sheet over $U$, then a chart $\phi :U\to \phi (U)\subseteq {\mathbb{R}}^n$ pulls back to the chart $\phi \circ p{\mathrm{\mid }}_S:S\to \phi (U)$. It is Hausdorff: points with different images are separated by inverse images of disjoint base neighborhoods, while distinct points in one fibre lie in distinct sheets over a common evenly covered neighborhood.

It remains to check second countability rather than silently assuming it. Fix a countable base $\mathcal{C}=\{C_j:j\in \mathbb{N}\}$ for $M$. By local path connectedness, the components of every $C_j$ are open by [F4]. For fixed $j$ these components form a countable family: each contains some $C_k$, and assigning to it the least such $k$ is injective because distinct components are disjoint. Thus all components of all the $C_j$ form a countable path-connected base. Its subfamily $\mathcal{U}$ consisting of members that are contained in an evenly covered coordinate domain is still countable and is a base, because such domains exist around every point and may first be refined by a $C_j$ and then by its component.

By [F3], $E$ is path connected. Fix ${\tilde{x}}_0\in E$. For each $U\in \mathcal{U}$, the sheets over $U$ form a countable family. Indeed, a path from ${\tilde{x}}_0$ to a point of a given sheet has compact parameter interval, so it can be subdivided into finitely many pieces whose projected images lie in members of $\mathcal{U}$. At each transition insert a member of $\mathcal{U}$ contained in the intersection of the two consecutive members. Starting with the sheet containing ${\tilde{x}}_0$, this finite string of indices determines each successive sheet uniquely: over a connected transition set, one sheet is connected and hence lies in exactly one sheet over the next base set. Finite strings of natural numbers are countable, and assigning to each sheet the least string that reaches it gives an injection into a countable set. No countable family of arbitrary choices is made.

The sheets over the countable base $\mathcal{U}$ therefore form a countable base for $E$. Together with step 1.1 this proves that $E$ is a topological $n$-manifold. On every such sheet use the pulled-back chart from step 1.1. If $(U,\phi )$ and $(V,\psi )$ are base charts, the transition between two overlapping pulled-back charts is the restriction of $\psi \circ {\phi }^{-1}$, because both sheet charts use the same projection $p$. Hence these charts form a smooth atlas, and [F5] gives a smooth structure for which $p$ is a smooth local diffeomorphism.

Conversely, in any smooth structure on the given topology for which $p$ is a local diffeomorphism, every sufficiently small sheet chart is exactly a pullback of a smooth base chart. It is therefore compatible with the atlas of step 3.1. The two maximal atlases coincide by [F5], proving uniqueness. The construction and all countability arguments are in ZF; after the empty case was discharged in step 1.1, the fixed point ${\tilde{x}}_0$ is one element of one nonempty space.