src/ZF/Zorn.thy

--- a/src/ZF/Zorn.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Zorn.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -197,14 +197,14 @@
 done
 
 lemma choice_super:
-     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
+     "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
       ==> ch ` super(S,X) \<in> super(S,X)"
 apply (erule apply_type)
 apply (unfold super_def maxchain_def, blast)
 done
 
 lemma choice_not_equals:
-     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
+     "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
       ==> ch ` super(S,X) \<noteq> X"
 apply (rule notI)
 apply (drule choice_super, assumption, assumption)
@@ -213,7 +213,7 @@
 
 text\<open>This justifies Definition 4.4\<close>
 lemma Hausdorff_next_exists:
-     "ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X) ==>
+     "ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X) ==>
       \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                    next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
 apply (rule_tac x="\<lambda>X\<in>Pow(S).
@@ -237,7 +237,7 @@
 text\<open>Lemma 4\<close>
 lemma TFin_chain_lemma4:
      "[| c \<in> TFin(S,next);
-         ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X);
+         ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X);
          next \<in> increasing(S);
          \<forall>X \<in> Pow(S). next`X =
                           if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
@@ -364,14 +364,14 @@
 text\<open>* Defining the "next" operation for Zermelo's Theorem *\<close>
 
 lemma choice_Diff:
-     "[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
+     "[| ch \<in> (\<Prod>X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
 apply (erule apply_type)
 apply (blast elim!: equalityE)
 done
 
 text\<open>This justifies Definition 6.1\<close>
 lemma Zermelo_next_exists:
-     "ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==>
+     "ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X) ==>
            \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                       next`X = (if X=S then S else cons(ch`(S-X), X))"
 apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
@@ -391,7 +391,7 @@
 
 text\<open>The construction of the injection\<close>
 lemma choice_imp_injection:
-     "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
+     "[| ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X);
          next \<in> increasing(S);
          \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
       ==> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))