src/ZF/AC/AC17_AC1.thy

 (* *********************************************************************** *)
 (* more properties of HH                                                   *)
 (* *********************************************************************** *)
 
 lemma UN_eq_imp_well_ord:
-     "[| x - (\<Union>j \<in> LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x}.  
+     "[| x - (\<Union>j \<in> \<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x}.  
         HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, j)) = 0;   
         f \<in> Pow(x)-{0} -> x |]   
         ==> \<exists>r. well_ord(x,r)"
 apply (rule exI)
 apply (erule well_ord_rvimage 

 done
 
 lemma AC17_AC1_aux1:
      "[| \<forall>f \<in> Pow(x) - {0} -> x. \<exists>u \<in> Pow(x) - {0}. f`u\<notin>u;   
          \<exists>f \<in> Pow(x)-{0}->x.  
-            x - (\<Union>a \<in> (LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).   
+            x - (\<Union>a \<in> (\<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).   
             HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,a)) = 0 |]  
         ==> P"
 apply (erule bexE)
 apply (erule UN_eq_imp_well_ord [THEN exE], assumption)
 apply (erule ex_choice_fun_Pow [THEN exE])

 apply (unfold AC17_def)
 apply (rule classical)
 apply (erule not_AC1_imp_ex [THEN exE])
 apply (case_tac 
        "\<exists>f \<in> Pow(x)-{0} -> x. 
-        x - (\<Union>a \<in> (LEAST i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
+        x - (\<Union>a \<in> (\<mu> i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
 apply (erule AC17_AC1_aux1, assumption)
 apply (drule AC17_AC1_aux2)
 apply (erule allE)
 apply (drule bspec, assumption)
 apply (drule AC17_AC1_aux4)