Theory Delta_System

section‹The Delta System Lemma\label{sec:dsl}›

theory Delta_System


text‹The ‹Delta System Lemma› (DSL) states that any uncountable family of
finite sets includes an uncountable delta system. This is the simplest
non trivial version; others, for cardinals greater than term‹ℵ⇘1⇙›  assume
some weak versions of the generalized continuum hypothesis for the
cardinals involved.

The proof is essentially the one in cite‹III.2.6› in "kunen2011set" for the
case  term‹ℵ⇘1⇙›; another similar presentation can be found in
cite‹Chap.~16› in "JW".›

lemma delta_system_Aleph1:
  assumes "AF. Finite(A)" "F  ℵ⇘1⇙"
  shows "D. D  F  delta_system(D)  D  ℵ⇘1⇙"
proof -
  text‹Since all members are finite,›
  from AF. Finite(A)
  have "(λAF. |A|) : F  ω" (is "?cards : _")
    by (rule_tac lam_type) simp
  moreover from this
  have a:"?cards -`` {n} = { AF . |A| = n }" for n
    using vimage_lam by auto
  note F  ℵ⇘1⇙›
  moreover from calculation
  text‹there are uncountably many have the same cardinal:›
  obtain n where "nω" "|?cards -`` {n}| = ℵ⇘1⇙"
    using eqpoll_Aleph1_cardinal_vimage[of F ?cards] by auto
  define G where "G  ?cards -`` {n}"
  moreover from calculation
  have "G  F" by auto
  text‹Therefore, without loss of generality, we can assume that all
  elements of the family have cardinality termnω.›
  have "AG  |A| = n" and "G  ℵ⇘1⇙" for A
    using cardinal_Card_eqpoll_iff by auto
  with nω
  text‹So we prove the result by induction on this termn and
  generalizing termG, since the argument requires changing the
  family in order to apply the inductive hypothesis.›
  have "D. D  G  delta_system(D)  D  ℵ⇘1⇙"
  proof (induct arbitrary:G)
    case 0 ― ‹This case is impossible›
    have "G  {0}"
      using cardinal_0_iff_0 by auto
    with G  ℵ⇘1⇙›
    show ?case
      using nat_lt_Aleph1 subset_imp_le_cardinal[of G "{0}"]
        lt_trans2 cardinal_Card_eqpoll_iff by auto
    case (succ n)
    have "aG. Finite(a)"
      using Finite_cardinal_iff' nat_into_Finite[of "succ(n)"]
      by fastforce
    show "D. D  G  delta_system(D)  D  ℵ⇘1⇙"
    proof (cases "p. {AG . p  A}  ℵ⇘1⇙")
      case True ― ‹the positive case, uncountably many sets with a
                    common element›
      obtain p where "{AG . p  A}  ℵ⇘1⇙" by blast
      moreover from this
      have "{A-{p} . A{XG. pX}}  ℵ⇘1⇙" (is "?F  _")
        using Diff_bij[of "{AG . p  A}" "{p}"]
          comp_bij[OF bij_converse_bij, where C="ℵ⇘1⇙"] by fast
      text‹Now using the hypothesis of the successor case,›
      moreover from A. AG  |A|=succ(n) aG. Finite(a)
        and this
      have "pA  AG  |A - {p}| = n" for A
        using Finite_imp_succ_cardinal_Diff[of _ p] by force
      moreover from this and nω
      have "a?F. Finite(a)"
        using Finite_cardinal_iff' nat_into_Finite by auto
      text‹we may apply the inductive hypothesis to the new family term?F:›
      note (A. A  ?F  |A| = n)  ?F  ℵ⇘1
             D. D  ?F  delta_system(D)  D  ℵ⇘1⇙›
      obtain D where "D{A-{p} . A{XG. pX}}" "delta_system(D)" "D  ℵ⇘1⇙"
        by auto
      moreover from this
      obtain r where "AD. BD. A  B  A  B = r"
        by fastforce
      have "AD.BD. A{p}  B{p}(A  {p})  (B  {p}) = r{p}"
        by blast
      have "delta_system({B  {p} . BD})" (is "delta_system(?D)")
        by fastforce
      moreover from D  ℵ⇘1⇙›
      have "|D| = ℵ⇘1⇙" "Infinite(D)"
        using cardinal_eqpoll_iff
        by (auto intro!: uncountable_iff_subset_eqpoll_Aleph1[THEN iffD2]
            uncountable_imp_Infinite) force
      moreover from this
      have "?D  ℵ⇘1⇙"
        using cardinal_map_Un[of D "{p}"] naturals_lt_nat
          cardinal_eqpoll_iff[THEN iffD1] by simp
      note D  {A-{p} . A{XG. pX}}
      have "?D  G"
      proof -
          fix A
          assume "AG" "pA"
          moreover from this
          have "A = A - {p}  {p}"
            by blast
          have "A -{p}  {p}  G"
            by auto
        with D  {A-{p} . A{XG. pX}}
        show ?thesis
          by blast
      show "D. D  G  delta_system(D)  D  ℵ⇘1⇙" by auto
      case False
      note ¬ (p. {A  G . p  A}  ℵ⇘1) ― ‹the other case›
      moreover from G  ℵ⇘1⇙›
      have "{A  G . p  A}  ℵ⇘1⇙" (is "?G(p)  _") for p
        by (blast intro:lepoll_eq_trans[OF subset_imp_lepoll])
      have "?G(p)  ℵ⇘1⇙" for p
        unfolding lesspoll_def by simp
      then (* may omit the previous step if unfolding here: *)
      have "?G(p)  ω" for p
        using lesspoll_aleph_plus_one[of 0] Aleph_zero_eq_nat by auto
      have "{A  G . S  A  0} = (pS. ?G(p))" for S
        by auto
      have "countable(S)  countable({A  G . S  A  0})" for S
        using InfCard_nat Card_nat
         le_Card_iff[THEN iffD2, THEN [3] lepoll_imp_cardinal_UN_le,
           THEN [2] le_Card_iff[THEN iffD1], of ω S]
        unfolding countable_def by simp
      text‹For every countable subfamily of termG there is another some
      element disjoint from all of them:›
      have "AG. SX. S  A = 0" if "|X| < ℵ⇘1⇙" "X  G" for X
      proof -
        from nω A. AG  |A| = succ(n)
        have "AG  Finite(A)" for A
          using cardinal_Card_eqpoll_iff
          unfolding Finite_def by fastforce
        with XG
        have "AX  countable(A)" for A
          using Finite_imp_countable by auto
        with |X| < ℵ⇘1⇙›
        have "countable(X)"
          using Card_nat[THEN cardinal_lt_csucc_iff, of X]
            countable_union_countable countable_iff_cardinal_le_nat
          unfolding Aleph_def by simp
        with countable(_)  countable({A  G . _   A  0})
        have "countable({A  G . (X)  A  0})" .
        with G  ℵ⇘1⇙›
        obtain B where "BG" "B  {A  G . (X)  A  0}" 
          using nat_lt_Aleph1 cardinal_Card_eqpoll_iff[of "ℵ⇘1⇙" G]
            uncountable_not_subset_countable[of "{A  G . (X)  A  0}" G]
          by auto
        show "AG. SX. S  A = 0" by auto
      moreover from G  ℵ⇘1⇙›
      obtain b where "bG"
        using uncountable_iff_subset_eqpoll_Aleph1
          uncountable_not_empty by blast
      text‹Hence, the hypotheses to perform a bounded-cardinal selection
      are satisfied,›
      obtain S where "S:ℵ⇘1G" "αℵ⇘1 βℵ⇘1 α<β  S`α  S`β = 0"
        for α β
        using bounded_cardinal_selection[of "ℵ⇘1⇙" G "λs a. s  a = 0" b]
        by force
      have "α  ℵ⇘1 β  ℵ⇘1 αβ  S`α  S`β = 0" for α β
        using lt_neq_symmetry[of "ℵ⇘1⇙" "λα β. S`α  S`β = 0"] Card_is_Ord
        by auto blast
      text‹and a symmetry argument shows that obtained termS is
      an injective  term‹ℵ⇘1⇙›-sequence of disjoint elements of termG.›
      moreover from this and A. AG  |A| = succ(n) S : ℵ⇘1 G
      have "S  inj(ℵ⇘1, G)"
        using cardinal_succ_not_0 Int_eq_zero_imp_not_eq[of "ℵ⇘1⇙" "λx. S`x"]
        unfolding inj_def by fastforce
      moreover from calculation
      have "range(S)  ℵ⇘1⇙"
        using inj_bij_range eqpoll_sym unfolding eqpoll_def by fast
      moreover from calculation
      have "range(S)  G"
        using inj_is_fun range_fun_subset_codomain by fast
      show "D. D  G  delta_system(D)  D  ℵ⇘1⇙"
        using inj_is_fun range_eq_image[of S "ℵ⇘1⇙" G]
          image_function[OF fun_is_function, OF inj_is_fun, of S "ℵ⇘1⇙" G]
          domain_of_fun[OF inj_is_fun, of S "ℵ⇘1⇙" G]
        by (rule_tac x="S``ℵ⇘1⇙" in exI) auto
      text‹This finishes the successor case and hence the proof.›
  with G  F
  show ?thesis by blast

lemma delta_system_uncountable:
  assumes "AF. Finite(A)" "uncountable(F)"
  shows "D. D  F  delta_system(D)  D  ℵ⇘1⇙"
proof -
  from assms
  obtain S where "S  F" "S  ℵ⇘1⇙"
    using uncountable_iff_subset_eqpoll_Aleph1[of F] by auto
  moreover from AF. Finite(A) and this
  have "AS. Finite(A)" by auto
  show ?thesis using delta_system_Aleph1[of S]
    by auto