It sounds like you are talking about Cantor's theorem, and its proof is here -> http://us.metamath.org/mpeuni/canth.html http://us.metamath.org/mpeuni/canth.htm

It sounds like you are talking about Cantor's theorem, and its proof is here -> http://us.metamath.org/mpeuni/canth.html http://us.metamath.org/mpeuni/canth.html . The formalization is both short and straightforward, so while you might argue that the axioms of set theory aren't intuitive enough, the fact that they come together to prove the impossibility of bijection between a set and its powerset is unassailable.