$\newcommand{\plcypmf}[2]{\pi(#1\,|\,#2)}$ $\newcommand{\condpmf}[2]{p(#1\,|\,#2)}$ $\newcommand{\condpmfsym}[3]{#1(#2\,|\,#3)}$ $\newcommand{\cpwrt}[3]{P_{#1}\{#2\:|\, #3\}}$ $\newcommand{\Ecwrt}[3]{E_{#1}[#2\:|\, #3]}$ $\newcommand{\argmax}[1]{\text{arg max}_{#1}\,}$ $\newcommand{\cases}[1]{\begin{cases}#1\end{cases}}$ $\newcommand{\mcalA}{\mathcal{A}}$ $\newcommand{\mcalR}{\mathcal{R}}$ $\newcommand{\mcalS}{\mathcal{S}}$ $\newcommand{\qd}{\quad}$ $\newcommand{\wR}{\mathbb{R}}$ $\newcommand{\Bop}{\Big(}$ $\newcommand{\Bcp}{\Big)}$ $\newcommand{\Prn}[1]{\Bop #1\Bcp}$ $\newcommand{\align}[1]{\begin{align*}#1\end{align*}}$ $\newcommand{\wes}{\blacksquare}$
We assume that the Markov Property holds:
$$\align{ &\condpmf{g_{t+1}}{s',a,s}=\condpmf{g_{t+1}}{s'} \\\\ &\condpmf{g_{t+1}}{s',r,a,s}=\condpmf{g_{t+1}}{s'}\tag{MDP.0} \\\\ &\condpmf{r_{t+2}}{s',a,s}=\condpmf{r_{t+2}}{s'} \\\\ }$$
Proposition MDP.5 Let $T$ be the time variable and let $t$ be a particular time. Let $s_0\in\mcalS$, let $a_0\in\mcalA(s)$, and let $\pi$ be any policy on $\mcalS$. Define the family of policies $\phi_T$ on $\mcalS$ by
$$ \cpwrt{\phi_T}{A_T=a}{S_T=s}=\condpmfsym{\phi_T}{a}{s}\equiv\cases{\condpmfsym{\pi}{a}{s}&\text{if }T\neq t\text{ or }s\neq s_0\\1&\text{else if }a=a_0\\0&\text{else}} $$
Then
$$ q_{\phi_{t}}(s_0,a_0) = q_{\pi}(s_0,a_0) \\ $$
Proof If $g_{t+1}$ is a possible outcome of $G_{t+1}$, then $\condpmf{g_{t+1}}{s',\phi_t}=\condpmf{g_{t+1}}{s',\pi}$ since $\phi_t=\pi$ for $T=t+1,t+2,\dots$. Also note that $\condpmf{s'}{s_0,a_0,\phi_t}=\condpmf{s'}{s_0,a_0,\pi}$. That is, if we know the state and action in the current time step, then the policy is irrelevant to determining the next state. Hence
$$\align{ q_{\phi_t}(s_0,a_0) &= \Ecwrt{\phi}{G_t}{S_t=s_0,A_t=a_0} \\ &= \Ecwrt{\phi_t}{R_{t+1}+\gamma G_{t+1}}{S_t=s_0,A_t=a_0} \\ &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a_0}+\Ecwrt{\phi_t}{\gamma G_{t+1}}{S_t=s_0,A_t=a_0} \\ &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\condpmf{g_{t+1}}{s_0,a_0,\phi_t} \\ &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',s_0,a_0,\phi_t}\cdot\condpmf{s'}{s_0,a_0,\phi_t} \\ &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',\phi_t}\cdot\condpmf{s'}{s_0,a_0,\phi_t}\tag{by MDP.0} \\ &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',\pi}\cdot\condpmf{s'}{s_0,a_0,\pi} \\ &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',s_0,a_0,\pi}\cdot\condpmf{s'}{s_0,a_0,\pi} \\ &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\condpmf{g_{t+1}}{s_0,a_0,\pi} \\ &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a_0}+\Ecwrt{\pi}{\gamma G_{t+1}}{S_t=s_0,A_t=a_0} \\ &= \Ecwrt{\pi}{R_{t+1}+\gamma G_{t+1}}{S_t=s_0,A_t=a_0} \\ &= \Ecwrt{\pi}{G_t}{S_t=s_0,A_t=a_0} \\ &= q_{\pi}(s_0,a_0) \\ }$$
$\wes$
Define $v_{*}:\mcalS\mapsto\wR$ by
$$ v_{*}(s)\equiv\max_{\pi}v_{\pi}(s)\qd\text{for all }s\in\mcalS $$
Define $q_{*}:\mcalS\times\mcalA\mapsto\wR$ by
$$ q_{*}(s,a)\equiv\max_{\pi}q_{\pi}(s,a)\qd\text{for all }s\in\mcalS,a\in\mcalA(s) $$
Proposition MDP.6 Let $s_0\in\mcalS$ and define $a_{*}$ by
$$ a_{*}\in\argmax{a\in\mcalA(s_0)}\Prn{\argmax{\pi}q_{\pi}(s_0,a)}=\argmax{a\in\mcalA(s_0)}q_{*}(s_0,a) $$
And define the policy $\pi_{**}$ by
$$ \pi_{**}\in\argmax{\pi}q_{\pi}(s_0,a_{*}) $$
And define the family of policies $\phi_T$ by
$$ \cpwrt{\phi_T}{A_T=a}{S_T=s}=\condpmfsym{\phi_T}{a}{s}\equiv\cases{\condpmfsym{\pi_{**}}{a}{s}&\text{if }T\neq t\text{ or }s\neq s_0\\1&\text{else if }a=a_{*}\\0&\text{else}} $$
Then $\phi_t$ is an optimal policy:
$$ \phi_t\in\argmax{\pi}v_{\pi}(s_0) $$
and
$$ v_{\phi_t}(s_0)=v_{*}(s_0)=\max_{\pi}v_{\pi}(s_0) $$
Proof For any policy $\pi$, we have
$$\align{ v_{\pi}(s_0) &= \sum_{a\in\mcalA(s_0)}\condpmfsym{\pi}{a}{s_0}\cdot q_{\pi}(s_0,a) \\ &\leq \sum_{a\in\mcalA(s_0)}\condpmfsym{\pi}{a}{s_0}\cdot q_{*}(s_0,a) \\ &\leq \sum_{a\in\mcalA(s_0)}\condpmfsym{\pi}{a}{s_0}\cdot q_{*}(s_0,a_{*}) \\ &= q_{*}(s_0,a_{*})\cdot\sum_{a\in\mcalA(s_0)}\condpmfsym{\pi}{a}{s_0} \\ &= q_{*}(s_0,a_{*}) \\ &= q_{\pi_{**}}(s_0,a_{*}) \\ &= q_{\phi_t}(s_0,a_{*})\tag{by MDP.5} \\ &= \sum_{a\in\mcalA(s_0)}\condpmfsym{\phi_t}{a}{s_0}\cdot q_{\phi_t}(s_0,a) \\ &= v_{\phi_t}(s_0) }$$
$\wes$
Proposition MDP.7 For all $s\in\mcalS$, we have
$$ v_{*}(s) = \max_{a\in\mcalA(s)}q_{*}(s,a) $$
Proof Let $s_0\in\mcalS$ and define $a_{*}\in\argmax{a\in\mcalA(s_0)}q_{*}(s_0,a)$. Then for any policy $\pi$, we have
$$\align{ v_{\pi}(s_0) &= \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{\pi}(s_0,a) \\ &\leq \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{*}(s_0,a) \\ &\leq \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{*}(s_0,a_{*}) \\ &= q_{*}(s_0,a_{*})\cdot\sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0} \\ &= q_{*}(s_0,a_{*}) \\ &= \max_{a\in\mcalA(s_0)}q_{*}(s_0,a) }$$
Since this is true for all policies $\pi$, then it must be that
$$ v_{*}(s_0)=\max_{\pi}v_{\pi}(s_0)\leq\max_{a\in\mcalA(s_0)}q_{*}(s_0,a) $$
Suppose, by way of contradiction, that we have strict inequality:
$$ v_{*}(s_0)\lt\max_{a\in\mcalA(s_0)}q_{*}(s_0,a) \tag{MDP.7.1} $$
Define the policy $\pi_{**}$ by
$$ \pi_{**}\in\argmax{\pi}q_{\pi}(s_0,a_{*}) $$
Then
$$ q_{\pi_{**}}(s_0,a_{*}) = \max_{\pi}q_{\pi}(s_0,a_{*}) = q_{*}(s_0,a_{*}) = \max_{a\in\mcalA(s_0)}q_{*}(s_0,a) $$
And MDP.6 gives the first equality:
$$ v_{\pi_{**}}(s_0)=\max_{\pi}v_{\pi}(s_0)=v_{*}(s_0)\lt\max_{a\in\mcalA(s_0)}q_{*}(s_0,a) $$
Also define the family of policies $\phi_T$ by
$$ \cpwrt{\phi_T}{A_T=a}{S_T=s}=\condpmfsym{\phi_T}{a}{s}\equiv\cases{\condpmfsym{\pi_{**}}{a}{s}&\text{if }T\neq t\text{ or }s\neq s_0\\1&\text{else if }a=a_{*}\\0&\text{else}} $$
Then MDP.5 gives the third equality:
$$\align{ v_{\phi_t}(s_0) = \sum_{a\in\mcalA(s_0)}\condpmfsym{\phi_t}{a}{s_0}q_{\phi_t}(s_0,a) = q_{\phi_t}(s_0,a_{*})= q_{\pi_{**}}(s_0,a_{*}) = \max_{a\in\mcalA(s_0)}q_{*}(s_0,a) \gt v_{*}(s_0) }$$
This contradicts the definition of $v_{*}(s_0)\equiv\max_{\pi}v_{\pi}(s_0)$. Hence assumption MDP.7.1 is false and we have
$$ v_{*}(s_0)=\max_{a\in\mcalA(s_0)}q_{*}(s_0,a) $$
Since $s_0\in\mcalS$ was chosen arbitrarily, then this equality holds for all $s\in\mcalS$.
$\wes$