src/HOL/BNF_Cardinal_Order_Relation.thy

  \<forall>i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
 
 lemma regularCard_UNION:
 assumes r: "Card_order r"   "regularCard r"
 and As: "relChain r As"
-and Bsub: "B \<le> (UN i : Field r. As i)"
+and Bsub: "B \<le> (\<Union>i \<in> Field r. As i)"
 and cardB: "|B| <o r"
 shows "\<exists>i \<in> Field r. B \<le> As i"
 proof-
   let ?phi = "\<lambda>b j. j \<in> Field r \<and> b \<in> As j"
   have "\<forall>b\<in>B. \<exists>j. ?phi b j" using Bsub by blast

     hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1)
     also have 22: "|Field ?r'| =o ?r'"
     using r' by (simp add: card_of_Field_ordIso[of ?r'])
     finally have "|K| \<le>o ?r'" .
     moreover
-    {let ?L = "UN j : K. underS ?r' j"
+    {let ?L = "\<Union> j \<in> K. underS ?r' j"
      let ?J = "Field r"
      have rJ: "r =o |?J|"
      using r_card card_of_Field_ordIso ordIso_symmetric by blast
      assume "|K| <o ?r'"
      hence "|K| <=o r" using r' card_of_Card_order[of K] by blast

 qed
 
 lemma cardSuc_UNION:
 assumes r: "Card_order r" and "\<not>finite (Field r)"
 and As: "relChain (cardSuc r) As"
-and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
+and Bsub: "B \<le> (\<Union> i \<in> Field (cardSuc r). As i)"
 and cardB: "|B| <=o r"
 shows "\<exists>i \<in> Field (cardSuc r). B \<le> As i"
 proof-
   let ?r' = "cardSuc r"
   have "Card_order ?r' \<and> |B| <o ?r'"