Existence of normal neighborhoods

Suppose $n\ge 1$. Choose one smooth chart $x:Q\to x(Q)\subseteq {\mathbb{R}}^n$ at $p$ and let $L:{\mathbb{R}}^n\to T_{p}M$ be the inverse of the chart-induced linear isomorphism $d{x}_p$. The local representative $F=x\circ {\exp }_p\circ L$ is defined and smooth on the open neighbourhood $L^{-1}({\mathcal{E}}_p\cap {\exp }_p^{-1}(Q))$ of $0$ by [F1]--[F2], satisfies $F(0)=x(p)$, and has derivative $DF(0)=d{x}_p\circ I\circ L=I$ by [F1]--[F2].

Apply [F3] to $F$. It yields open neighbourhoods $P$ of $0$ and $W$ of $x(p)$ on which $F$ is a diffeomorphism. Since $P$ is open about $0$, choose $r>0$ with $B(0,r)\subseteq P$. Put ${\tilde{U}}_p=L(B(0,r))$. This set is open and star-shaped about $0_p$, and the restriction of ${\exp }_p$ is a diffeomorphism onto its image: it is the chart conjugate of the restriction of $F{\mathrm{\mid }}_P$, whose inverse remains smooth. Its image $U_p$ is open because $F(B(0,r))$ is open in $W$ under the homeomorphism $F{\mathrm{\mid }}_P$, and $x^{-1}$ is a chart homeomorphism. Finally $0_p\in {\tilde{U}}_p$ and ${\exp }_p(0_p)=p$, so $p\in U_p$.

If $n=0$, a manifold chart shows that $\{p\}$ is open and $T_{p}M=\{0_p\}$. Take ${\tilde{U}}_p=\{0_p\}$ and $U_p=\{p\}$; the exponential is the unique bijection and both it and its inverse are smooth under the zero-dimensional convention. Dimension one is included in steps 1.1--2.1. An empty manifold has no $p$, so the universal statement is vacuous. The source ball is open, so no sphere endpoint is included, and it contains the degenerate zero vector. ${\mathrm{A}\mathrm{C}}_{\omega }$ is used only through [F1]; the choice-free inverse theorem [F3] and choosing one chart and one positive radius for the fixed $p$ require no family choice.