In his paper "Qualitative Distinctions Between Some Toposes of Generalized Graphs" (reproduced here), page 267, Lawvere says that the idempotent-splitting completion of the category of open sets of Euclidean spaces $\mathbb{R}^n$ and smooth maps between them is the category of smooth (paracompact, Hausdorff) manifolds and smooth maps.

It's not very hard to see that every smooth manifold is a smooth retract of such an open set, so that the category of smooth manifolds embeds fully and faithfully in the idempotent-splitting completion. However, I haven't been able to find a proof of the converse, that every smooth retract of an open set is in fact a smooth manifold. Equivalently: if $p: U \to U$ is a smooth map on an open set $U$ of $\mathbb{R}^n$ such that $p \circ p = p$, then the fixed-point set $Fix(p) = \{x \in U: p(x) = x\}$ admits a smooth structure so that the inclusion $Fix(p) \hookrightarrow U$ is a smooth embedding. Can someone provide details of a proof?

In his paper "Qualitative Distinctions Between Some Toposes of Generalized Graphs" (reproduced here), page 267, Lawvere says that the idempotent-splitting completion of the category of open sets of Euclidean spaces $\mathbb{R}^n$ and smooth maps between them is the category of smooth (second-countable, Hausdorff) manifolds and smooth maps.

It's not very hard to see that every smooth manifold is a smooth retract of such an open set, so that the category of smooth manifolds embeds fully and faithfully in the idempotent-splitting completion. However, I haven't been able to find a proof of the converse, that every smooth retract of an open set is in fact a smooth manifold. Equivalently: if $p: U \to U$ is a smooth map on an open set $U$ of $\mathbb{R}^n$ such that $p \circ p = p$, then the fixed-point set $Fix(p) = \{x \in U: p(x) = x\}$ admits a smooth structure so that the inclusion $Fix(p) \hookrightarrow U$ is a smooth embedding. Can someone provide details of a proof?