Did Stephen Cook see the significance of showing that SAT is NP-Hard before actually proving it?
First of all, Cook actually showed that the problem of whether a logical expression is a tautology is $\mathbb{NP}$-complete under Cook reductions. The proof however works by replacing them with Karp reductions to show that $SAT$ is $\mathbb{NP}$-complete, in the modern sense of the term.

As for whether Cook understood the significance of a $\mathbb{NP}$-complete problem not being in $\mathbb{P}$, going through the actual paper  shows that he did. However, I believe it wasn't until Karp's list of 21 complete problems that the practical significance of Cook's result began to be understood.