# HG changeset patch
# User lcp
# Date 785757759 -3600
# Node ID ba231bd734d212c28524ff48280713f46440943d
# Parent  bdc06678106330933b6774788af152af74d2fe71
moved Cantors theorem here from ZF/ex/misc

diff -r bdc066781063 -r ba231bd734d2 src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Fri Nov 25 10:43:50 1994 +0100
+++ b/src/ZF/ZF.ML	Fri Nov 25 11:02:39 1994 +0100
@@ -20,6 +20,7 @@
   val bexI		: thm
   val bex_cong		: thm
   val bspec		: thm
+  val cantor		: thm
   val CollectD1		: thm
   val CollectD2		: thm
   val CollectE		: thm
@@ -480,6 +481,17 @@
 (*Standard claset*)
 val lemmas_cs = subset0_cs addSIs [subsetI] addEs [subsetCE];
 
+(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
+
+val cantor_cs = FOL_cs   (*precisely the rules needed for the proof*)
+  addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI]
+  addSEs [CollectE, equalityCE];
+
+(*The search is undirected; similar proof attempts may fail.
+  b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *)
+val cantor = prove_goal ZF.thy "EX S: Pow(A). ALL x:A. b(x) ~= S"
+ (fn _ => [best_tac cantor_cs 1]);
+
 (*Lemma for the inductive definition in Zorn.thy*)
 val Union_in_Pow = prove_goal ZF.thy
     "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"