diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -65,6 +65,26 @@
 
 abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
 
+lemma disjoint_family_elem_disjnt:
+  assumes "infinite A" "finite C"
+      and df: "disjoint_family_on B A"
+  obtains x where "x \<in> A" "disjnt C (B x)"
+proof -
+  have "False" if *: "\<forall>x \<in> A. \<exists>y. y \<in> C \<and> y \<in> B x"
+  proof -
+    obtain g where g: "\<forall>x \<in> A. g x \<in> C \<and> g x \<in> B x"
+      using * by metis
+    with df have "inj_on g A"
+      by (fastforce simp add: inj_on_def disjoint_family_on_def)
+    then have "infinite (g ` A)"
+      using \<open>infinite A\<close> finite_image_iff by blast
+    then show False
+      by (meson \<open>finite C\<close> finite_subset g image_subset_iff)
+  qed
+  then show ?thesis
+    by (force simp: disjnt_iff intro: that)
+qed
+
 lemma disjoint_family_onD:
   "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
   by (auto simp: disjoint_family_on_def)