>> This is because TSP is not in NP

Um, the decision version of TSP (does there exist a Hamilton path of length at most x?) is definitely in NP. It is also NP-hard (your definition of NP-hardness is wrong).

I guess what you're trying to say is that the optimization version of TSP (find the shortest Hamilton path) cannot be verified in polynomial time, as this would require answering the decision version of TSP in the negative for some length x, and this is hard to verify since TSP is not in co-NP.

In spirit, your comment is absolutely spot on. But as we all know, technically correct is the best kind of correct :)