src/HOL/Cardinals/Cardinal_Order_Relation.thy

 proof(rule ccontr, auto)
   have 0: "wo_rel r" and 00: "Well_order r"
   unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
   have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
   have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
-  using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
+  using AsB L apply safe by (metis "0" UN_I subsetD wo_rel.isLimOrd_succ)
   assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
   have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
   proof safe
     fix i j assume 1: "(i, j) \<in> r" "i \<noteq> j" and Asij: "As i = As j"
     hence rij: "(succ r i, j) \<in> r" by (metis "0" wo_rel.succ_smallest)