This isn't about the "meat" of your post, but: for someone who's finding Cantor's theorem hard to believe, it might be worth avoiding proof by contradiction, which can be confusing. I'd rather say "Let f be any element of (2^X)^X. Define S_f(x) = 1 - f(x)(x). Then for any x, f(x)(x) != S_f(x), which means f(x) != S_f. So for every f, there's an S_f such that there's no x that represents it."
I wouldn't normally link to a post from my math blog here, but it concerns a cute interpretation of Cantor's theorem that showed up when I was thinking about program equilibria at the April MIRI workshop, so I thought it might be of interest here (e.g. if you're trying to persuade a mathematically inclined friend of yours to attend a future workshop). A short proof of the undecidability of the halting problem falls out as a bonus.