# HG changeset patch
# User wenzelm
# Date 1466436308 -7200
# Node ID 814541a57d89fd856fbaf96188105f556a822637
# Parent  bc1f17d45e9127ca66c704fda4e8531d752df135
tuned proof;

diff -r bc1f17d45e91 -r 814541a57d89 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Jun 20 17:03:50 2016 +0200
+++ b/src/HOL/Fun.thy	Mon Jun 20 17:25:08 2016 +0200
@@ -793,15 +793,15 @@
 
 subsection \<open>Cantor's Paradox\<close>
 
-lemma Cantors_paradox: "\<not> (\<exists>f. f ` A = Pow A)"
-proof clarify
-  fix f
-  assume "f ` A = Pow A"
-  then have *: "Pow A \<subseteq> f ` A" by blast
+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" unfolding Pow_def by auto
-  with * obtain x where "x \<in> A \<and> f x = ?X" by blast
-  then show False by best
+  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