[_rpd]

> This is completely uncontroversial

I think it is still intuitively surprising that some infinite sets somehow have more elements than other infinite sets. The powerset operator is very special because it can create this difference.

[Smaug123]

I suppose I really meant "why should one expect that f might be injective anyway?" Once you're no longer in the context of a set like N which is very familiar, there's just no obvious reason for the theorem to be false.