Let $M$ be a $k$-dimensional embedded $C^\alpha$-submanifold of $\mathbb R^d$ with boundary, i.e. $M$ is locally $\mathcal C^\alpha$-diffeomorphic$^1$ to $\mathbb H^k:=\mathbb R^{k-1}\times[0,\infty)$.
Let $x\in\partial M$ so that there is a boundary chart $(\Omega,\phi)$ of $M$ around $x$, i.e. $\Omega$ is an open subset of $M$ and $\phi$ is a $C^\alpha$-diffeomorphism from $\Omega$ onto an open subset of $\mathbb H^k$ with $\phi(x)\in\partial\mathbb H^k=\mathbb R^{k-1}\times\{0\}$.
Now let $\tilde\Omega:=\Omega\cap\partial M$ and $\tilde\phi:=\pi\circ\left.\phi\right|_{\tilde\Omega}$.$^2$ It's easy to show that $$\tilde\phi(\tilde\Omega)=\phi(\Omega)\cap\partial\mathbb H^k\tag1.$$
How can we show that $(\tilde\Omega,\tilde\phi)$ is an interior chart of $\partial M$, i.e. $\tilde\phi$ is a $C^\alpha$-diffeomorphism from the open subset $\tilde\Omega$ of $\partial M$ onto the open subset $\tilde\phi(\tilde\Omega)$ of $\mathbb R^{k-1}$?
It's easy to show that $\tilde\Omega$ is $\partial M$-open and $\tilde\phi(\tilde\Omega)$ is $\mathbb R^{k-1}$-open. How can we show that they are $C^\alpha$-diffeomorphic and how can we determine the (Fréchet) derivative ${\rm D}\tilde\phi$ in terms of ${\rm D}\phi$?
It's clear$^3$ that $\tilde\phi$ is a homeomorphism from $\tilde\Omega$ onto $\tilde\phi(\tilde\Omega)$, where both are enquipped with the corresponding subspace topology.
But how can we show the $C^\alpha$-differentiability? We may note that $$\left.\iota\circ\pi\right|_{\partial\mathbb H^k}=\operatorname{id}_{\partial\mathbb H^k}\tag2$$ and so I would expect that $${\rm D}\tilde\phi(x)=\pi\circ{\rm D}\phi(x)\circ\iota\circ\pi\;\;\;\text{for all }x\in\tilde\Omega\subseteq\partial\mathbb H^k\tag3.$$ Analogously, it should hold $${\rm D}\tilde\phi^{-1}(u)={\rm D}\phi^{-1}(\iota u)\circ\iota\;\;\;\text{for all }u\in\tilde\phi(\tilde\Omega)\tag4.$$ My problem in proving this rigorously is that all we know is that $\phi$ and $\phi^{-1}$ extend locally to (Fréchet) differentiable functions. I guess everything works out fine, but I think we need to be careful.
$^1$ If $E_i$ is a $\mathbb R$-Banach space and $B_i\subseteq E_i$, then $f:B_1\to E_2$ is called $C^\alpha$-differentiable at $x_1\in B_1$ if there is an $E_1$-open neighborhood $\Omega_1$ of $x_1$ and a $\tilde f\in\mathcal C^\alpha(\Omega_1,E_2)$ with $\left.f\right|_{B_1\:\cap\:\Omega_1}=\left.\tilde f\right|_{B_1\:\cap\:\Omega_1}$. $f$ is called $\mathcal C^\alpha$-differentiable if $f$ is $C^\alpha$-differentiable at $x_1$ for all $x_1\in B_1$.
$g$ is called $C^\alpha$-diffeomorphism from $B_1$ onto $B_2$ if $g$ is a homeomorphism from $B_1$ onto $B_2$ and $g$ and $g^{-1}$ are $C^\alpha$-differentiable.
$^2$ For convenience, let $\iota$ denote the canonical embedding of $\mathbb R^{k-1}$ onto $\mathbb R^k$ with $\iota\mathbb R^{k-1}=\mathbb R^{k-1}\times\{0\}$ and $\pi$ denote the canonical projection of $\mathbb R^k$ onto $\mathbb R^{k-1}$ with $\pi(\mathbb R^{k-1}\times\{0\})=\mathbb R^{k-1}$.
$^3$ see, for example, https://proofwiki.org/wiki/Restriction_of_Continuous_Mapping_is_Continuous/Topological_Spaces.