Theorem 17.7 of Jech's Set Theory is Kunen's theorem:
If $j : V \to M$ is a nontrivial elementary embedding, then $M \neq V$.
My main issue lies in one line of the proof, which says:
The cardinal $\lambda$ is the limit of a sequence of measurable cardinals and hence is a strong limit cardinal. Since $\operatorname{cf}\lambda = \omega$, $2^\lambda = \lambda^{\aleph_0}$.
I don't think it is entirely clear why this identity holds, which is vital in the proof as we need exactly this to invoke Lemma 17.8. This is especially the case if the reader does not read Jech from start to finish, and thus may not be familiar with infinite products of cardinals (I came from the 2011 edition of Kunen, which does not cover infinite product).
We first have $\lambda^{\aleph_0} \leq (2^{\lambda})^{\aleph_0} = 2^{\lambda \cdot \aleph_0} = 2^\lambda$ (this always holds). On the other hand, since $\operatorname{cf}\lambda = \omega$, there exists a sequence of $\langle\gamma_n : n \in \omega\rangle$ such that $\gamma_n < \lambda$ for all $n$, and $\sup\{\gamma_n : n \in \omega\} = \lambda$. In the spirit of Theorem 5.16 of Jech, we have: $$ 2^\lambda = \prod_n 2^{\gamma_n} \leq \prod_n \lambda = \lambda^{\aleph_0} $$ where the middle $\leq$ follows from that $\lambda$ is a strong limit.