Equivalence of sphere and arbitrary-atlas pullback formulations

Let $S^4=\{x\in\mathbb R^5:\|x\|=1\}$, with its subspace topology and standard stereographic smooth structure modeled on $\mathbb R^4$. The following two universal assertions are logically equivalent, with every quantified underlying type lying in the base universe. The first says that for every $M$ among the compact Hausdorff topological spaces equipped with a specified charted-space structure modeled on $\mathbb R^4$ whose chart transitions are $C^\infty$ for the identity model on $\mathbb R^4$, existence of a homeomorphism $M\to S^4$ implies existence of a diffeomorphism $M\to S^4$, where a diffeomorphism is a bijection for which both the forward map and the inverse are $C^\infty$ in the specified manifold charts. The second says that for every $N$ among the same class of spaces, with its specified smooth atlas $A$, and every homeomorphism $e:N\to S^4$, there exists a self-homeomorphism $h:N\to N$ preserving the smooth structure from $A$ to the atlas pulled back along $e$. This target atlas consists exactly of charts $d\circ e$, for sphere atlas charts $d$, with inverse $e^{-1}\circ d^{-1}$ and preferred chart at $x$ induced by the sphere's preferred chart at $e(x)$. Preservation requires that for every source atlas chart $c$ and sphere atlas chart $d$, the open partial chart representative $(d\circ e)\circ h\circ c^{-1}$ and its inverse are smooth on their domains. The existential $h$ may depend on $e$ and need not be the identity; neither assertion requires uniqueness. No extra premise is imposed on this equivalence. Empty spaces are included in the universal space quantifiers, but have no homeomorphism to $S^4$, so the relevant implications and quantification over such homeomorphisms are vacuous for them.