Every nonempty path-connected locally path-connected semilocally simply connected space has a universal cover

Given: The objects, hypotheses, and choice principles stated above.

If $X$ is nonempty, path-connected, locally path-connected, and semilocally simply connected, then after a basepoint is fixed the path-class basic sets define a topology on $\tilde{X}$ for which the endpoint projection $p:\tilde{X}\to X$ is a covering map. (For a nonempty path-connected locally path-connected semilocally simply connected space, the path-class projection is a covering map).

A universal covering space of $B$ is a covering map $p:\tilde{B}\to B$ whose total space $\tilde{B}$ is simply connected (def-covering-map-and-evenly-covered-neighbourhoods, def-simply-connected). (Universal covering spaces).

A topological space $X$ is simply connected when it is nonempty and path-connected (def-path-connected) and, for every $x_0\in X$, the group ${\pi }_1(X,x_0)$ has exactly one element. (Simply connected topological spaces).

For a covering $p:(E,e_0)\to (B,b_0)$, the induced homomorphism $p_{\ast }:{\pi }_1(E,e_0)\to {\pi }_1(B,b_0)$ is injective. (A covering map induces an injective homomorphism on fundamental groups).