A closed smooth manifold has the homotopy type of a finite CW complex

(Critical values and regular levels.) If $M=\mathrm{\varnothing }$, the empty CW complex has no cells and the identity is a homotopy equivalence, proving the claim. Hence assume $M\mathrm{\ne }\mathrm{\varnothing }$. By [F1] choose an excellent Morse function $f:M\to \mathbb{R}$; this is a single existential instantiation from the hypothesis that one exists, and the Axiom of Choice is what supplies that existence [F1]. By [F2] $f$ has finitely many critical points, so its set of critical values is finite, say $c_1<\cdots <c_k$; the values $c_j$ are distinct by excellence [F3]. Since a value of $f$ is critical exactly when it is the image of a critical point, every real number different from $c_1,\dots ,c_k$ is a regular value. Choose $a_0<c_1$, then $a_j\in (c_j,c_{j+1})$ for $1\le j\le k-1$, and $a_k>c_k$; these are finitely many choices from nonempty open intervals, the last possible because $M$ is compact so $f$ is bounded [F3]. Then $M^{a_0}=\mathrm{\varnothing }$ and $M^{a_k}=M$.

(One critical point per band.) Fix $j\in \{1,\dots ,k\}$. The band $f^{-1}([a_{j-1},a_j])$ is a closed subset of the compact manifold $M$, hence compact, its boundary values $a_{j-1}<a_j$ are regular, and it contains exactly the one critical point $p_j$ of $f$, which is nondegenerate of some index ${\lambda }_j$ because $f$ is Morse [F3]. The hypotheses of the one-critical-point attachment statement are therefore satisfied, and it provides a homotopy equivalence from $M^{a_j}$ to $M^{a_{j-1}}$ with one ${\lambda }_j$-cell attached, compatible with the lower sublevel [F4]. Suppose inductively that $M^{a_{j-1}}\simeq X_{j-1}$, with $X_{j-1}$ finite CW. Transport the attaching map through that equivalence using F8. For ${\lambda }_j>0$, cellular approximation F7 homotopes the transported sphere map into $X_{j-1}^{{\lambda }_j-1}$; F8 preserves the attachment homotopy type. Adjoining the ${\lambda }_j$-cell along this cellular map gives a finite CW complex $X_j$. If ${\lambda }_j=0$, adjoin one isolated vertex. Starting with $X_0=\mathrm{\varnothing }$, this proves the induction, including out-of-index-order critical points.

(Conclusion.) Taking $j=k$ gives $M=M^{a_k}\simeq X_k$, and $X_k$ is a finite CW complex with exactly $k$ cells, one for each critical point [F5]. The Axiom of Choice is used only through the existence of the excellent Morse function [F1] and through the countable choice principle consumed by the handle attachment statement, which follows from full AC by [F6]. Hence $M$ has the homotopy type of a finite CW complex.