More details on NP \subset PSPACE:

Spoiler

We define co-NP to be the set of languages where if w is not in L, then this can be verified in polynomial time (for a fixed polynomial). So in particular, if P = NP, then NP = co-NP (as the decider for a language L could be used as the verifier for membership and non-membership). By the contrapositive, if we knew that NP != co-NP, we would have that P != NP. This is why our second result that NP = co-NP is so important.

Note that just because we can efficiently verify membership and non-membership does not mean we can decide in polynomial time. That is, we do not have that P = NP.

Link: https://arxiv.org/pdf/1609.09562v1.pdf