diff -r 207b6fcfc47d -r d1c26efb7a47 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Oct 10 19:07:54 2022 +0200
+++ b/src/HOL/Set.thy	Tue Oct 11 10:45:42 2022 +0200
@@ -952,6 +952,16 @@
 lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
   by auto
 
+theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
+proof
+  assume "\<exists>f. f ` A = Pow A"
+  then obtain f where f: "f ` A = Pow A" ..
+  let ?X = "{a \<in> A. a \<notin> f a}"
+  have "?X \<in> Pow A" by blast
+  then have "?X \<in> f ` A" by (simp only: f)
+  then obtain x where "x \<in> A" and "f x = ?X" by blast
+  then show False by blast
+qed
 
 text \<open>\<^medskip> Range of a function -- just an abbreviation for image!\<close>