A space admitting a universal covering is semilocally simply connected

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

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 space $X$ is semilocally simply connected at $x\in X$ when there is a neighbourhood $U$ of $x$ and a basepoint-preserving inclusion $(U,x)\hookrightarrow (X,x)$ whose induced map on fundamental groups is trivial (def-neighbourhood-top, def-induced-homomorphism-on-fundamental-groups, def-based-loops-and-fundamental-group). It is semilocally simply connected when this holds at every point. The neighbourhood need not itself be simply connected. (Semilocally simply connected spaces with explicit basepoint convention).

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).

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).