diff --git a/thys/Delta_System_Lemma/Cardinal_Library.thy b/thys/Delta_System_Lemma/Cardinal_Library.thy
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/Cardinal_Library.thy
@@ -0,0 +1,708 @@
+section\<open>Cardinal Arithmetic under Choice\label{sec:cardinal-lib}\<close>
+
+theory Cardinal_Library
+  imports
+    ZF_Library
+    ZF.Cardinal_AC
+
+begin
+
+text\<open>This theory includes results on cardinalities that depend on $\AC$\<close>
+
+
+subsection\<open>Results on cardinal exponentiation\<close>
+
+text\<open>Non trivial instances of cardinal exponentiation require that
+     the relevant function spaces are well-ordered, hence this 
+     implies a strong use of choice.\<close>
+
+lemma cexp_eqpoll_cong:
+  assumes
+    "A \<approx> A'" "B \<approx> B'"
+  shows
+    "A\<^bsup>\<up>B\<^esup> = A'\<^bsup>\<up>B'\<^esup>"
+  unfolding cexp_def using cardinal_eqpoll_iff
+    function_space_eqpoll_cong assms
+  by simp
+
+lemma cexp_cexp_cmult: "(\<kappa>\<^bsup>\<up>\<nu>1\<^esup>)\<^bsup>\<up>\<nu>2\<^esup> = \<kappa>\<^bsup>\<up>\<nu>2 \<otimes> \<nu>1\<^esup>"
+proof -
+  have "(\<kappa>\<^bsup>\<up>\<nu>1\<^esup>)\<^bsup>\<up>\<nu>2\<^esup> = (\<nu>1 \<rightarrow> \<kappa>)\<^bsup>\<up>\<nu>2\<^esup>"
+    using cardinal_eqpoll
+    by (intro cexp_eqpoll_cong) (simp_all add:cexp_def)
+  also
+  have " \<dots> = \<kappa>\<^bsup>\<up>\<nu>2 \<times> \<nu>1\<^esup>"
+    unfolding cexp_def using curry_eqpoll cardinal_cong by blast
+  also
+  have " \<dots> = \<kappa>\<^bsup>\<up>\<nu>2 \<otimes> \<nu>1\<^esup>"
+    using cardinal_eqpoll[THEN eqpoll_sym]
+    unfolding cmult_def by (intro cexp_eqpoll_cong) (simp)
+  finally
+  show ?thesis  .
+qed
+
+lemma cardinal_Pow: "|Pow(X)| = 2\<^bsup>\<up>X\<^esup>" \<comment> \<open>Perhaps it's better with |X|\<close>
+  using cardinal_eqpoll_iff[THEN iffD2, OF Pow_eqpoll_function_space]
+  unfolding cexp_def by simp
+
+lemma cantor_cexp:
+  assumes "Card(\<nu>)"
+  shows "\<nu> < 2\<^bsup>\<up>\<nu>\<^esup>"
+  using assms Card_is_Ord Card_cexp
+proof (intro not_le_iff_lt[THEN iffD1] notI)
+  assume "2\<^bsup>\<up>\<nu>\<^esup> \<le> \<nu>"
+  then
+  have "|Pow(\<nu>)| \<le> \<nu>"
+    using cardinal_Pow by simp
+  with assms
+  have "Pow(\<nu>) \<lesssim> \<nu>"
+    using cardinal_eqpoll_iff Card_le_imp_lepoll Card_cardinal_eq
+    by auto
+  then
+  obtain g where "g \<in> inj(Pow(\<nu>), \<nu>)"
+    by blast
+  then
+  show "False"
+    using cantor_inj by simp
+qed simp
+
+lemma cexp_left_mono:
+  assumes "\<kappa>1 \<le> \<kappa>2"
+  shows "\<kappa>1\<^bsup>\<up>\<nu>\<^esup> \<le> \<kappa>2\<^bsup>\<up>\<nu>\<^esup>"
+    (* \<comment> \<open>short, unreadable proof: \<close>
+  unfolding cexp_def
+  using subset_imp_lepoll[THEN lepoll_imp_Card_le]
+    assms le_subset_iff[THEN iffD1, OF assms]
+    Pi_weaken_type[of _ _ "\<lambda>_. \<kappa>1" "\<lambda>_. \<kappa>2"] by auto *)
+proof -
+  from assms
+  have "\<kappa>1 \<subseteq> \<kappa>2"
+    using le_subset_iff by simp
+  then
+  have "\<nu> \<rightarrow> \<kappa>1  \<subseteq> \<nu> \<rightarrow> \<kappa>2"
+    using Pi_weaken_type by auto
+  then
+  show ?thesis unfolding cexp_def
+    using lepoll_imp_Card_le subset_imp_lepoll by simp
+qed
+
+lemma cantor_cexp':
+  assumes "2 \<le> \<kappa>" "Card(\<nu>)"
+  shows "\<nu> < \<kappa>\<^bsup>\<up>\<nu>\<^esup>"
+  using cexp_left_mono assms cantor_cexp lt_trans2 by blast
+
+lemma InfCard_cexp:
+  assumes "2 \<le> \<kappa>" "InfCard(\<nu>)"
+  shows "InfCard(\<kappa>\<^bsup>\<up>\<nu>\<^esup>)"
+  using assms cantor_cexp'[THEN leI] le_trans Card_cexp
+  unfolding InfCard_def by auto
+
+lemmas InfCard_cexp' = InfCard_cexp[OF nats_le_InfCard, simplified]
+  \<comment> \<open>\<^term>\<open>InfCard(\<kappa>) \<Longrightarrow> InfCard(\<nu>) \<Longrightarrow> InfCard(\<kappa>\<^bsup>\<up>\<nu>\<^esup>)\<close>\<close>
+
+
+subsection\<open>Miscellaneous\<close>
+
+lemma cardinal_RepFun_le: "|{f(a) . a\<in>A}| \<le> |A|"
+proof -
+  have "(\<lambda>x\<in>A. f(x)) \<in> surj(A, {f(a) . a\<in>A})"
+    unfolding surj_def using lam_funtype by auto
+  then
+  show ?thesis
+    using  surj_implies_cardinal_le by blast
+qed
+
+lemma subset_imp_le_cardinal: "A \<subseteq> B \<Longrightarrow> |A| \<le> |B|"
+  using subset_imp_lepoll[THEN lepoll_imp_Card_le] .
+
+lemma lt_cardinal_imp_not_subset: "|A| < |B| \<Longrightarrow> \<not> B \<subseteq> A"
+  using subset_imp_le_cardinal le_imp_not_lt by blast
+
+lemma cardinal_lt_csucc_iff: "Card(K) \<Longrightarrow> |K'| < K\<^sup>+ \<longleftrightarrow> |K'| \<le> K"
+  by (simp add: Card_lt_csucc_iff)
+
+lemma cardinal_UN_le_nat:
+  "(\<And>i. i\<in>\<omega> \<Longrightarrow> |X(i)| \<le> \<omega>) \<Longrightarrow> |\<Union>i\<in>\<omega>. X(i)| \<le> \<omega>"
+  by (simp add: cardinal_UN_le InfCard_nat)
+
+lemma leqpoll_imp_cardinal_UN_le:
+  notes [dest] = InfCard_is_Card Card_is_Ord
+  assumes "InfCard(K)" "J \<lesssim> K" "\<And>i. i\<in>J \<Longrightarrow> |X(i)| \<le> K"
+  shows "|\<Union>i\<in>J. X(i)| \<le> K"
+proof -
+  from \<open>J \<lesssim> K\<close>
+  obtain f where "f \<in> inj(J,K)" by blast
+  define Y where "Y(k) \<equiv> if k\<in>range(f) then X(converse(f)`k) else 0" for k
+  have "i\<in>J \<Longrightarrow> f`i \<in> K" for i
+    using inj_is_fun[OF \<open>f \<in> inj(J,K)\<close>] by auto
+  have "(\<Union>i\<in>J. X(i)) \<subseteq> (\<Union>i\<in>K. Y(i))"
+  proof (standard, elim UN_E)
+    fix x i
+    assume "i\<in>J" "x\<in>X(i)"
+    with \<open>f \<in> inj(J,K)\<close> \<open>i\<in>J \<Longrightarrow> f`i \<in> K\<close>
+    have "x \<in> Y(f`i)" "f`i \<in> K"
+      unfolding Y_def
+      using inj_is_fun[OF \<open>f \<in> inj(J,K)\<close>]
+        right_inverse apply_rangeI by auto
+    then
+    show "x \<in> (\<Union>i\<in>K. Y(i))" by auto
+  qed
+  then
+  have "|\<Union>i\<in>J. X(i)| \<le> |\<Union>i\<in>K. Y(i)|"
+    unfolding Y_def using subset_imp_le_cardinal by simp
+  with assms \<open>\<And>i. i\<in>J \<Longrightarrow> f`i \<in> K\<close>
+  show "|\<Union>i\<in>J. X(i)| \<le> K"
+    using inj_converse_fun[OF \<open>f \<in> inj(J,K)\<close>] unfolding Y_def
+    by (rule_tac le_trans[OF _ cardinal_UN_le]) (auto intro:Ord_0_le)+
+qed
+
+lemma cardinal_lt_csucc_iff':
+  includes Ord_dests
+  assumes "Card(\<kappa>)"
+  shows "\<kappa> < |X| \<longleftrightarrow> \<kappa>\<^sup>+ \<le> |X|"
+  using assms cardinal_lt_csucc_iff[of \<kappa> X] Card_csucc[of \<kappa>]
+    not_le_iff_lt[of "\<kappa>\<^sup>+" "|X|"] not_le_iff_lt[of "|X|" \<kappa>]
+  by blast
+
+lemma lepoll_imp_subset_bij: "X \<lesssim> Y \<longleftrightarrow> (\<exists>Z. Z \<subseteq> Y \<and> Z \<approx> X)"
+proof
+  assume "X \<lesssim> Y"
+  then
+  obtain j where  "j \<in> inj(X,Y)"
+    by blast
+  then
+  have "range(j) \<subseteq> Y" "j \<in> bij(X,range(j))"
+    using inj_bij_range inj_is_fun range_fun_subset_codomain
+    by blast+
+  then
+  show "\<exists>Z. Z \<subseteq> Y \<and> Z \<approx> X"
+    using eqpoll_sym unfolding eqpoll_def
+    by force
+next
+  assume "\<exists>Z. Z \<subseteq> Y \<and> Z \<approx> X"
+  then
+  obtain Z f where "f \<in> bij(Z,X)" "Z \<subseteq> Y"
+    unfolding eqpoll_def by force
+  then
+  have "converse(f) \<in> inj(X,Y)"
+    using bij_is_inj inj_weaken_type bij_converse_bij by blast
+  then
+  show "X \<lesssim> Y" by blast
+qed
+
+text\<open>The following result proves to be very useful when combining
+     \<^term>\<open>cardinal\<close> and \<^term>\<open>eqpoll\<close> in a calculation.\<close>
+
+lemma cardinal_Card_eqpoll_iff: "Card(\<kappa>) \<Longrightarrow> |X| = \<kappa> \<longleftrightarrow> X \<approx> \<kappa>"
+  using Card_cardinal_eq[of \<kappa>] cardinal_eqpoll_iff[of X \<kappa>] by auto
+    \<comment> \<open>Compare @{thm "le_Card_iff"}\<close>
+
+lemma lepoll_imp_lepoll_cardinal: assumes "X \<lesssim> Y" shows "X \<lesssim> |Y|"
+  using assms cardinal_Card_eqpoll_iff[of "|Y|" Y]
+    lepoll_eq_trans[of _ _ "|Y|"] by simp
+
+lemma lepoll_Un:
+  assumes "InfCard(\<kappa>)" "A \<lesssim> \<kappa>" "B \<lesssim> \<kappa>"
+  shows "A \<union> B \<lesssim> \<kappa>"
+proof -
+  have "A \<union> B \<lesssim> sum(A,B)"
+    using Un_lepoll_sum .
+  moreover
+  note assms
+  moreover from this
+  have "|sum(A,B)| \<le> \<kappa> \<oplus> \<kappa>"
+    using sum_lepoll_mono[of A \<kappa> B \<kappa>] lepoll_imp_Card_le
+    unfolding cadd_def by auto
+  ultimately
+  show ?thesis
+    using InfCard_cdouble_eq Card_cardinal_eq
+      InfCard_is_Card Card_le_imp_lepoll[of "sum(A,B)" \<kappa>]
+      lepoll_trans[of "A\<union>B"]
+    by auto
+qed
+
+lemma cardinal_Un_le:
+  assumes "InfCard(\<kappa>)" "|A| \<le> \<kappa>" "|B| \<le> \<kappa>"
+  shows "|A \<union> B| \<le> \<kappa>"
+  using assms lepoll_Un le_Card_iff InfCard_is_Card by auto
+
+text\<open>This is the unconditional version under choice of 
+     @{thm Cardinal.Finite_cardinal_iff}.\<close>
+lemma Finite_cardinal_iff': "Finite(|i|) \<longleftrightarrow> Finite(i)"
+  using cardinal_eqpoll_iff eqpoll_imp_Finite_iff by fastforce
+
+lemma cardinal_subset_of_Card:
+  assumes "Card(\<gamma>)" "a \<subseteq> \<gamma>"
+  shows "|a| < \<gamma> \<or> |a| = \<gamma>"
+proof -
+  from assms
+  have "|a| < |\<gamma>| \<or> |a| = |\<gamma>|"
+    using subset_imp_le_cardinal le_iff by simp
+  with assms
+  show ?thesis
+    using Card_cardinal_eq by simp
+qed
+
+lemma cardinal_cases:
+  includes Ord_dests
+  shows "Card(\<gamma>) \<Longrightarrow> |X| < \<gamma> \<longleftrightarrow> \<not> |X| \<ge> \<gamma>"
+  using not_le_iff_lt
+  by auto
+
+
+subsection\<open>Countable and uncountable sets\<close>
+
+\<comment> \<open>Kunen's Definition I.10.5\<close>
+definition
+  countable :: "i\<Rightarrow>o" where
+  "countable(X) \<equiv> X \<lesssim> \<omega>"
+
+lemma countableI[intro]: "X \<lesssim> \<omega> \<Longrightarrow> countable(X)"
+  unfolding countable_def by simp
+
+lemma countableD[dest]: "countable(X) \<Longrightarrow> X \<lesssim> \<omega>"
+  unfolding countable_def by simp
+
+lemma countable_iff_cardinal_le_nat: "countable(X) \<longleftrightarrow> |X| \<le> \<omega>"
+  using le_Card_iff[of \<omega> X] Card_nat
+  unfolding countable_def by simp
+
+lemma lepoll_countable: "X \<lesssim> Y \<Longrightarrow> countable(Y) \<Longrightarrow> countable(X)"
+  using lepoll_trans[of X Y] by blast
+
+\<comment> \<open>Next lemma can be proved without using AC\<close>
+lemma surj_countable: "countable(X) \<Longrightarrow> f \<in> surj(X,Y) \<Longrightarrow> countable(Y)"
+  using surj_implies_cardinal_le[of f X Y, THEN le_trans]
+    countable_iff_cardinal_le_nat by simp
+
+lemma Finite_imp_countable: "Finite(X) \<Longrightarrow> countable(X)"
+  unfolding Finite_def
+  by (auto intro:InfCard_nat nats_le_InfCard[of _ \<omega>,
+        THEN le_imp_lepoll] dest!:eq_lepoll_trans[of X _ \<omega>])
+
+lemma countable_imp_countable_UN:
+  assumes "countable(J)" "\<And>i. i\<in>J \<Longrightarrow> countable(X(i))"
+  shows "countable(\<Union>i\<in>J. X(i))"
+  using assms leqpoll_imp_cardinal_UN_le[of \<omega> J X] InfCard_nat
+    countable_iff_cardinal_le_nat
+  by auto
+
+lemma countable_union_countable:
+  assumes "\<And>x. x \<in> C \<Longrightarrow> countable(x)" "countable(C)"
+  shows "countable(\<Union>C)"
+  using assms countable_imp_countable_UN[of C "\<lambda>x. x"] by simp
+
+abbreviation
+  uncountable :: "i\<Rightarrow>o" where
+  "uncountable(X) \<equiv> \<not> countable(X)"
+
+lemma uncountable_iff_nat_lt_cardinal:
+  "uncountable(X) \<longleftrightarrow> \<omega> < |X|"
+  using countable_iff_cardinal_le_nat not_le_iff_lt by simp
+
+lemma uncountable_not_empty: "uncountable(X) \<Longrightarrow> X \<noteq> 0"
+  using empty_lepollI by auto
+
+lemma uncountable_imp_Infinite: "uncountable(X) \<Longrightarrow> Infinite(X)"
+  using uncountable_iff_nat_lt_cardinal[of X] lepoll_nat_imp_Infinite[of X]
+    cardinal_le_imp_lepoll[of \<omega> X] leI
+  by simp
+
+lemma uncountable_not_subset_countable:
+  assumes "countable(X)" "uncountable(Y)"
+  shows "\<not> (Y \<subseteq> X)"
+  using assms lepoll_trans subset_imp_lepoll[of Y X]
+  by blast
+
+
+subsection\<open>Results on Alephs\<close>
+
+lemma nat_lt_Aleph1: "\<omega> < \<aleph>\<^bsub>1\<^esub>"
+  by (simp add: Aleph_def lt_csucc)
+
+lemma zero_lt_Aleph1: "0 < \<aleph>\<^bsub>1\<^esub>"
+  by (rule lt_trans[of _ "\<omega>"], auto simp add: ltI nat_lt_Aleph1)
+
+lemma le_aleph1_nat: "Card(k) \<Longrightarrow> k<\<aleph>\<^bsub>1\<^esub> \<Longrightarrow> k \<le> \<omega>"
+  by (simp add: Aleph_def Card_lt_csucc_iff Card_nat)
+
+lemma Aleph_succ: "\<aleph>\<^bsub>succ(\<alpha>)\<^esub> = \<aleph>\<^bsub>\<alpha>\<^esub>\<^sup>+"
+  unfolding Aleph_def by simp
+
+lemma lesspoll_aleph_plus_one:
+  assumes "Ord(\<alpha>)"
+  shows "d \<prec> \<aleph>\<^bsub>succ(\<alpha>)\<^esub> \<longleftrightarrow> d \<lesssim> \<aleph>\<^bsub>\<alpha>\<^esub>"
+  using assms lesspoll_csucc Aleph_succ Card_is_Ord by simp
+
+lemma cardinal_Aleph [simp]: "Ord(\<alpha>) \<Longrightarrow> |\<aleph>\<^bsub>\<alpha>\<^esub>| = \<aleph>\<^bsub>\<alpha>\<^esub>"
+  using Card_cardinal_eq by simp
+
+\<comment> \<open>Could be proved without using AC\<close>
+lemma Aleph_lesspoll_increasing:
+  includes Aleph_intros
+  shows "a < b \<Longrightarrow> \<aleph>\<^bsub>a\<^esub> \<prec> \<aleph>\<^bsub>b\<^esub>"
+  using cardinal_lt_iff_lesspoll[of "\<aleph>\<^bsub>a\<^esub>" "\<aleph>\<^bsub>b\<^esub>"] Card_cardinal_eq[of "\<aleph>\<^bsub>b\<^esub>"]
+    lt_Ord lt_Ord2 Card_Aleph[THEN Card_is_Ord] by auto
+
+lemma uncountable_iff_subset_eqpoll_Aleph1:
+  includes Ord_dests
+  notes Aleph_zero_eq_nat[simp] Card_nat[simp] Aleph_succ[simp]
+  shows "uncountable(X) \<longleftrightarrow> (\<exists>S. S \<subseteq> X \<and> S \<approx> \<aleph>\<^bsub>1\<^esub>)"
+proof
+  assume "uncountable(X)"
+  then
+  have "\<aleph>\<^bsub>1\<^esub> \<lesssim> X"
+    using uncountable_iff_nat_lt_cardinal cardinal_lt_csucc_iff'
+      cardinal_le_imp_lepoll by force
+  then
+  obtain S where "S \<subseteq> X" "S \<approx> \<aleph>\<^bsub>1\<^esub>"
+    using lepoll_imp_subset_bij by auto
+  then
+  show "\<exists>S. S \<subseteq> X \<and> S \<approx> \<aleph>\<^bsub>1\<^esub>"
+    using cardinal_cong Card_csucc[of \<omega>] Card_cardinal_eq by auto
+next
+  assume "\<exists>S. S \<subseteq> X \<and> S \<approx> \<aleph>\<^bsub>1\<^esub>"
+  then
+  have "\<aleph>\<^bsub>1\<^esub> \<lesssim> X"
+    using subset_imp_lepoll[THEN [2] eq_lepoll_trans, of "\<aleph>\<^bsub>1\<^esub>" _ X,
+        OF eqpoll_sym] by auto
+  then
+  show "uncountable(X)"
+    using Aleph_lesspoll_increasing[of 0 1, THEN [2] lesspoll_trans1,
+        of "\<aleph>\<^bsub>1\<^esub>"] lepoll_trans[of "\<aleph>\<^bsub>1\<^esub>" X \<omega>]
+    by auto
+qed
+
+lemma lt_Aleph_imp_cardinal_UN_le_nat: "function(G) \<Longrightarrow> domain(G) \<lesssim> \<omega> \<Longrightarrow>
+   \<forall>n\<in>domain(G). |G`n|<\<aleph>\<^bsub>1\<^esub> \<Longrightarrow> |\<Union>n\<in>domain(G). G`n|\<le>\<omega>"
+proof -
+  assume "function(G)"
+  let ?N="domain(G)" and ?R="\<Union>n\<in>domain(G). G`n"
+  assume "?N \<lesssim> \<omega>"
+  assume Eq1: "\<forall>n\<in>?N. |G`n|<\<aleph>\<^bsub>1\<^esub>"
+  {
+    fix n
+    assume "n\<in>?N"
+    with Eq1 have "|G`n| \<le> \<omega>"
+      using le_aleph1_nat by simp
+  }
+  then
+  have "n\<in>?N \<Longrightarrow> |G`n| \<le> \<omega>" for n .
+  with \<open>?N \<lesssim> \<omega>\<close>
+  show ?thesis
+    using InfCard_nat leqpoll_imp_cardinal_UN_le by simp
+qed
+
+lemma Aleph1_eq_cardinal_vimage: "f:\<aleph>\<^bsub>1\<^esub>\<rightarrow>\<omega> \<Longrightarrow> \<exists>n\<in>\<omega>. |f-``{n}| = \<aleph>\<^bsub>1\<^esub>"
+proof -
+  assume "f:\<aleph>\<^bsub>1\<^esub>\<rightarrow>\<omega>"
+  then
+  have "function(f)" "domain(f) = \<aleph>\<^bsub>1\<^esub>" "range(f)\<subseteq>\<omega>"
+    by (simp_all add: domain_of_fun fun_is_function range_fun_subset_codomain)
+  let ?G="\<lambda>n\<in>range(f). f-``{n}"
+  from \<open>f:\<aleph>\<^bsub>1\<^esub>\<rightarrow>\<omega>\<close>
+  have "range(f) \<subseteq> \<omega>" by (simp add: range_fun_subset_codomain)
+  then
+  have "domain(?G) \<lesssim> \<omega>"
+    using subset_imp_lepoll by simp
+  have "function(?G)" by (simp add:function_lam)
+  from \<open>f:\<aleph>\<^bsub>1\<^esub>\<rightarrow>\<omega>\<close>
+  have "n\<in>\<omega> \<Longrightarrow> f-``{n} \<subseteq> \<aleph>\<^bsub>1\<^esub>" for n
+    using Pi_vimage_subset by simp
+  with \<open>range(f) \<subseteq> \<omega>\<close>
+  have "\<aleph>\<^bsub>1\<^esub> = (\<Union>n\<in>range(f). f-``{n})"
+  proof (intro equalityI, intro subsetI)
+    fix x
+    assume "x \<in> \<aleph>\<^bsub>1\<^esub>"
+    with \<open>f:\<aleph>\<^bsub>1\<^esub>\<rightarrow>\<omega>\<close> \<open>function(f)\<close> \<open>domain(f) = \<aleph>\<^bsub>1\<^esub>\<close>
+    have "x \<in> f-``{f`x}" "f`x \<in> range(f)"
+      using function_apply_Pair vimage_iff apply_rangeI by simp_all
+    then
+    show "x \<in> (\<Union>n\<in>range(f). f-``{n})" by auto
+  qed auto
+  {
+    assume "\<forall>n\<in>range(f). |f-``{n}| < \<aleph>\<^bsub>1\<^esub>"
+    then
+    have "\<forall>n\<in>domain(?G). |?G`n| < \<aleph>\<^bsub>1\<^esub>"
+      using zero_lt_Aleph1 by (auto)
+    with \<open>function(?G)\<close> \<open>domain(?G) \<lesssim> \<omega>\<close>
+    have "|\<Union>n\<in>domain(?G). ?G`n|\<le>\<omega>"
+      using lt_Aleph_imp_cardinal_UN_le_nat by blast
+    then
+    have "|\<Union>n\<in>range(f). f-``{n}|\<le>\<omega>" by simp
+    with \<open>\<aleph>\<^bsub>1\<^esub> = _\<close>
+    have "|\<aleph>\<^bsub>1\<^esub>| \<le> \<omega>" by simp
+    then
+    have "\<aleph>\<^bsub>1\<^esub> \<le> \<omega>"
+      using Card_Aleph Card_cardinal_eq
+      by simp
+    then
+    have "False"
+      using nat_lt_Aleph1 by (blast dest:lt_trans2)
+  }
+  with \<open>range(f)\<subseteq>\<omega>\<close>
+  obtain n where "n\<in>\<omega>" "\<not>(|f -`` {n}| < \<aleph>\<^bsub>1\<^esub>)"
+    by blast
+  moreover from this
+  have "\<aleph>\<^bsub>1\<^esub> \<le> |f-``{n}|"
+    using not_lt_iff_le Card_is_Ord by auto
+  moreover
+  note \<open>n\<in>\<omega> \<Longrightarrow> f-``{n} \<subseteq> \<aleph>\<^bsub>1\<^esub>\<close>
+  ultimately
+  show ?thesis
+    using subset_imp_le_cardinal[THEN le_anti_sym, of _ "\<aleph>\<^bsub>1\<^esub>"]
+      Card_Aleph Card_cardinal_eq by auto
+qed
+
+\<comment> \<open>There is some asymmetry between assumptions and conclusion
+    (\<^term>\<open>(\<approx>)\<close> versus \<^term>\<open>cardinal\<close>)\<close>
+lemma eqpoll_Aleph1_cardinal_vimage:
+  assumes "X \<approx> \<aleph>\<^bsub>1\<^esub>" "f : X \<rightarrow> \<omega>"
+  shows "\<exists>n\<in>\<omega>. |f-``{n}| = \<aleph>\<^bsub>1\<^esub>"
+proof -
+  from assms
+  obtain g where "g\<in>bij(\<aleph>\<^bsub>1\<^esub>,X)"
+    using eqpoll_sym by blast
+  with \<open>f : X \<rightarrow> \<omega>\<close>
+  have "f O g : \<aleph>\<^bsub>1\<^esub> \<rightarrow> \<omega>" "converse(g) \<in> bij(X, \<aleph>\<^bsub>1\<^esub>)"
+    using bij_is_fun comp_fun bij_converse_bij by blast+
+  then
+  obtain n where "n\<in>\<omega>" "|(f O g)-``{n}| = \<aleph>\<^bsub>1\<^esub>"
+    using Aleph1_eq_cardinal_vimage by auto
+  then
+  have "\<aleph>\<^bsub>1\<^esub> = |converse(g) `` (f -``{n})|"
+    using image_comp converse_comp
+    unfolding vimage_def by simp
+  also from \<open>converse(g) \<in> bij(X, \<aleph>\<^bsub>1\<^esub>)\<close> \<open>f: X\<rightarrow> \<omega>\<close>
+  have "\<dots> = |f -``{n}|"
+    using range_of_subset_eqpoll[of "converse(g)" X  _ "f -``{n}"]
+      bij_is_inj cardinal_cong bij_is_fun eqpoll_sym Pi_vimage_subset
+    by fastforce
+  finally
+  show ?thesis using \<open>n\<in>\<omega>\<close> by auto
+qed
+
+
+subsection\<open>Applications of transfinite recursive constructions\<close>
+
+definition
+  rec_constr :: "[i,i] \<Rightarrow> i" where
+  "rec_constr(f,\<alpha>) \<equiv> transrec(\<alpha>,\<lambda>a g. f`(g``a))"
+
+text\<open>The function \<^term>\<open>rec_constr\<close> allows to perform \<^emph>\<open>recursive
+     constructions\<close>: given a choice function on the powerset of some
+     set, a transfinite sequence is created by successively choosing
+     some new element.
+
+     The next result explains its use.\<close>
+
+lemma rec_constr_unfold: "rec_constr(f,\<alpha>) = f`({rec_constr(f,\<beta>). \<beta>\<in>\<alpha>})"
+  using def_transrec[OF rec_constr_def, of f \<alpha>] image_lam by simp
+
+lemma rec_constr_type: assumes "f:Pow(G)\<rightarrow> G" "Ord(\<alpha>)"
+  shows "rec_constr(f,\<alpha>) \<in> G"
+  using assms(2,1)
+  by (induct rule:trans_induct)
+    (subst rec_constr_unfold, rule apply_type[of f "Pow(G)" "\<lambda>_. G"], auto)
+
+text\<open>The next lemma is an application of recursive constructions.
+     It works under the assumption that whenever the already constructed
+     subsequence is small enough, another element can be added.\<close>
+
+lemma bounded_cardinal_selection:
+  includes Ord_dests
+  assumes
+    "\<And>X. |X| < \<gamma> \<Longrightarrow> X \<subseteq> G \<Longrightarrow> \<exists>a\<in>G. \<forall>s\<in>X. Q(s,a)" "b\<in>G" "Card(\<gamma>)"
+  shows
+    "\<exists>S. S : \<gamma> \<rightarrow> G \<and> (\<forall>\<alpha> \<in> \<gamma>. \<forall>\<beta> \<in> \<gamma>.  \<alpha><\<beta> \<longrightarrow> Q(S`\<alpha>,S`\<beta>))"
+proof -
+  let ?cdlt\<gamma>="{X\<in>Pow(G) . |X|<\<gamma>}" \<comment> \<open>“cardinal less than \<^term>\<open>\<gamma>\<close>”\<close>
+    and ?inQ="\<lambda>Y.{a\<in>G. \<forall>s\<in>Y. Q(s,a)}"
+  from assms
+  have "\<forall>Y \<in> ?cdlt\<gamma>. \<exists>a. a \<in> ?inQ(Y)"
+    by blast
+  then
+  have "\<exists>f. f \<in> Pi(?cdlt\<gamma>,?inQ)"
+    using AC_ball_Pi[of ?cdlt\<gamma> ?inQ] by simp
+  then
+  obtain f where f_type:"f \<in> Pi(?cdlt\<gamma>,?inQ)"
+    by auto
+  moreover
+  define Cb where "Cb \<equiv> \<lambda>_\<in>Pow(G)-?cdlt\<gamma>. b"
+  moreover from \<open>b\<in>G\<close>
+  have "Cb \<in> Pow(G)-?cdlt\<gamma> \<rightarrow> G"
+    unfolding Cb_def by simp
+  moreover
+  note \<open>Card(\<gamma>)\<close>
+  ultimately
+  have "f \<union> Cb : (\<Prod>x\<in>Pow(G). ?inQ(x) \<union> G)" using
+      fun_Pi_disjoint_Un[ of f ?cdlt\<gamma>  ?inQ Cb "Pow(G)-?cdlt\<gamma>" "\<lambda>_.G"]
+      Diff_partition[of "{X\<in>Pow(G). |X|<\<gamma>}" "Pow(G)", OF Collect_subset]
+    by auto
+  moreover
+  have "?inQ(x) \<union> G = G" for x by auto
+  ultimately
+  have "f \<union> Cb : Pow(G) \<rightarrow> G" by simp
+  define S where "S\<equiv>\<lambda>\<alpha>\<in>\<gamma>. rec_constr(f \<union> Cb, \<alpha>)"
+  from \<open>f \<union> Cb: Pow(G) \<rightarrow> G\<close> \<open>Card(\<gamma>)\<close>
+  have "S : \<gamma> \<rightarrow> G"
+    using Ord_in_Ord unfolding S_def
+    by (intro lam_type rec_constr_type) auto
+  moreover
+  have "\<forall>\<alpha>\<in>\<gamma>. \<forall>\<beta>\<in>\<gamma>. \<alpha> < \<beta> \<longrightarrow> Q(S ` \<alpha>, S ` \<beta>)"
+  proof (intro ballI impI)
+    fix \<alpha> \<beta>
+    assume "\<beta>\<in>\<gamma>"
+    with \<open>Card(\<gamma>)\<close>
+    have "{rec_constr(f \<union> Cb, x) . x\<in>\<beta>} = {S`x . x \<in> \<beta>}"
+      using Ord_trans[OF _ _ Card_is_Ord, of _ \<beta> \<gamma>]
+      unfolding S_def
+      by auto
+    moreover from \<open>\<beta>\<in>\<gamma>\<close> \<open>S : \<gamma> \<rightarrow> G\<close> \<open>Card(\<gamma>)\<close>
+    have "{S`x . x \<in> \<beta>} \<subseteq> G"
+      using Ord_trans[OF _ _ Card_is_Ord, of _ \<beta> \<gamma>]
+        apply_type[of S \<gamma> "\<lambda>_. G"] by auto
+    moreover from \<open>Card(\<gamma>)\<close> \<open>\<beta>\<in>\<gamma>\<close>
+    have "|{S`x . x \<in> \<beta>}| < \<gamma>"
+      using cardinal_RepFun_le[of \<beta>]  Ord_in_Ord
+        lt_trans1[of "|{S`x . x \<in> \<beta>}|" "|\<beta>|" \<gamma>]
+        Card_lt_iff[THEN iffD2, of \<beta> \<gamma>, OF _ _ ltI]
+      by force
+    moreover
+    have "\<forall>x\<in>\<beta>. Q(S`x, f ` {S`x . x \<in> \<beta>})"
+    proof -
+      from calculation and f_type
+      have "f ` {S`x . x \<in> \<beta>} \<in> {a\<in>G. \<forall>x\<in>\<beta>. Q(S`x,a)}"
+        using apply_type[of f ?cdlt\<gamma> ?inQ "{S`x . x \<in> \<beta>}"]
+        by blast
+      then
+      show ?thesis by simp
+    qed
+    moreover
+    assume "\<alpha>\<in>\<gamma>" "\<alpha> < \<beta>"
+    moreover
+    note \<open>\<beta>\<in>\<gamma>\<close> \<open>Cb \<in> Pow(G)-?cdlt\<gamma> \<rightarrow> G\<close>
+    ultimately
+    show "Q(S ` \<alpha>, S ` \<beta>)"
+      using fun_disjoint_apply1[of "{S`x . x \<in> \<beta>}" Cb f]
+        domain_of_fun[of Cb] ltD[of \<alpha> \<beta>]
+      by (subst (2) S_def, auto) (subst rec_constr_unfold, auto)
+  qed
+  ultimately
+  show ?thesis by blast
+qed
+
+text\<open>The following basic result can, in turn, be proved by a
+     bounded-cardinal selection.\<close>
+lemma Infinite_iff_lepoll_nat: "Infinite(X) \<longleftrightarrow> \<omega> \<lesssim> X"
+proof
+  assume "Infinite(X)"
+  then
+  obtain b where "b\<in>X"
+    using Infinite_not_empty by auto
+  {
+    fix Y
+    assume "|Y| < \<omega>"
+    then
+    have "Finite(Y)"
+      using Finite_cardinal_iff' ltD nat_into_Finite by blast
+    with \<open>Infinite(X)\<close>
+    have "X \<noteq> Y" by auto
+  }
+  with \<open>b\<in>X\<close>
+  obtain S where "S : \<omega> \<rightarrow> X"  "\<forall>\<alpha>\<in>\<omega>. \<forall>\<beta>\<in>\<omega>. \<alpha> < \<beta> \<longrightarrow> S`\<alpha> \<noteq> S`\<beta>"
+    using bounded_cardinal_selection[of \<omega> X "\<lambda>x y. x\<noteq>y"]
+      Card_nat by blast
+  moreover from this
+  have "\<alpha> \<in> \<omega> \<Longrightarrow> \<beta> \<in> \<omega> \<Longrightarrow> \<alpha>\<noteq>\<beta> \<Longrightarrow> S`\<alpha> \<noteq> S`\<beta>" for \<alpha> \<beta>
+    by (rule_tac lt_neq_symmetry[of "\<omega>" "\<lambda>\<alpha> \<beta>. S`\<alpha> \<noteq> S`\<beta>"])
+      auto
+  ultimately
+  show "\<omega> \<lesssim> X"
+    unfolding lepoll_def inj_def by blast
+qed (intro lepoll_nat_imp_Infinite)
+
+lemma Infinite_InfCard_cardinal: "Infinite(X) \<Longrightarrow> InfCard(|X|)"
+  using lepoll_eq_trans eqpoll_sym lepoll_nat_imp_Infinite
+    Infinite_iff_lepoll_nat Inf_Card_is_InfCard cardinal_eqpoll
+  by simp
+
+lemma Finite_to_one_surj_imp_cardinal_eq:
+  assumes "F \<in> Finite_to_one(X,Y) \<inter> surj(X,Y)" "Infinite(X)"
+  shows "|Y| = |X|"
+proof -
+  from \<open>F \<in> Finite_to_one(X,Y) \<inter> surj(X,Y)\<close>
+  have "X = (\<Union>y\<in>Y. {x\<in>X . F`x = y})"
+    using apply_type by fastforce
+  show ?thesis
+  proof (cases "Finite(Y)")
+    case True
+    with \<open>X = (\<Union>y\<in>Y. {x\<in>X . F`x = y})\<close> and assms
+    show ?thesis
+      using Finite_RepFun[THEN [2] Finite_Union, of Y "\<lambda>y. {x\<in>X . F`x = y}"]
+      by auto
+  next
+    case False
+    moreover from this
+    have "Y \<lesssim> |Y|"
+      using cardinal_eqpoll eqpoll_sym eqpoll_imp_lepoll by simp
+    moreover
+    note assms
+    moreover from calculation
+    have "y \<in> Y \<Longrightarrow> |{x\<in>X . F`x = y}| \<le> |Y|" for y
+      using Infinite_imp_nats_lepoll[THEN lepoll_imp_Card_le, of Y
+          "|{x\<in>X . F`x = y}|"] cardinal_idem by auto
+    ultimately
+    have "|\<Union>y\<in>Y. {x\<in>X . F`x = y}| \<le> |Y|"
+      using leqpoll_imp_cardinal_UN_le[of "|Y|" Y]
+        Infinite_InfCard_cardinal[of Y] by simp
+    moreover from \<open>F \<in> Finite_to_one(X,Y) \<inter> surj(X,Y)\<close>
+    have "|Y| \<le> |X|"
+      using surj_implies_cardinal_le by auto
+    moreover
+    note \<open>X = (\<Union>y\<in>Y. {x\<in>X . F`x = y})\<close>
+    ultimately
+    show ?thesis
+      using le_anti_sym by auto
+  qed
+qed
+
+lemma cardinal_map_Un:
+  assumes "Infinite(X)" "Finite(b)"
+  shows "|{a \<union> b . a \<in> X}| = |X|"
+proof -
+  have "(\<lambda>a\<in>X. a \<union> b) \<in> Finite_to_one(X,{a \<union> b . a \<in> X})"
+    "(\<lambda>a\<in>X. a \<union> b) \<in>  surj(X,{a \<union> b . a \<in> X})"
+    unfolding surj_def
+  proof
+    fix d
+    have "Finite({a \<in> X . a \<union> b = d})" (is "Finite(?Y(b,d))")
+      using \<open>Finite(b)\<close>
+    proof (induct arbitrary:d)
+      case 0
+      have "{a \<in> X . a \<union> 0 = d} = (if d\<in>X then {d} else 0)"
+        by auto
+      then
+      show ?case by simp
+    next
+      case (cons c b)
+      from \<open>c \<notin> b\<close>
+      have "?Y(cons(c,b),d) \<subseteq> (if c\<in>d then ?Y(b,d) \<union> ?Y(b,d-{c}) else 0)"
+        by auto
+      with cons
+      show ?case
+        using subset_Finite
+        by simp
+    qed
+    moreover
+    assume "d \<in> {x \<union> b . x \<in> X}"
+    ultimately
+    show "Finite({a \<in> X . (\<lambda>x\<in>X. x \<union> b) ` a = d})"
+      by simp
+  qed (auto intro:lam_funtype)
+  with assms
+  show ?thesis
+    using Finite_to_one_surj_imp_cardinal_eq by fast
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Delta_System_Lemma/Cofinality.thy b/thys/Delta_System_Lemma/Cofinality.thy
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/Cofinality.thy
@@ -0,0 +1,1205 @@
+section\<open>Cofinality\label{sec:cofinality}\<close>
+
+theory Cofinality
+  imports
+    ZF_Library
+begin
+
+
+subsection\<open>Basic results and definitions\<close>
+
+text\<open>A set \<^term>\<open>X\<close> is \<^emph>\<open>cofinal\<close> in \<^term>\<open>A\<close> (with respect to the relation
+    \<^term>\<open>r\<close>) if every element of \<^term>\<open>A\<close> is “bounded
+    above” by some element of \<^term>\<open>X\<close>. Note that \<^term>\<open>X\<close> does not need 
+    to be a subset of \<^term>\<open>A\<close>.\<close>
+definition
+  cofinal :: "[i,i,i] \<Rightarrow> o" where
+  "cofinal(X,A,r) \<equiv> \<forall>a\<in>A. \<exists>x\<in>X. \<langle>a,x\<rangle>\<in>r \<or> a = x"
+
+(*
+(* Alternative definitions *)
+definition
+  cofinal_predic :: "[i,i,[i,i]\<Rightarrow>o] \<Rightarrow> o" where
+  "cofinal_predic(X,A,r) \<equiv> \<forall>a\<in>A. \<exists>x\<in>X. r(a,x) \<or> a = x"
+
+definition
+  f_cofinal :: "[i\<Rightarrow>i,i,i,i] \<Rightarrow> o" where
+  "f_cofinal(f,C,A,r) \<equiv> \<forall>a\<in>A. \<exists>x\<in>C. \<langle>a,f(x)\<rangle>\<in>r \<or> a = f(x)"
+
+(* The next definition doesn't work if 0 is the top element of A.
+   But it works for limit ordinals. *)
+definition
+  cofinal_fun' :: "[i,i,i] \<Rightarrow> o" where
+  "cofinal_fun'(f,A,r) == f_cofinal(\<lambda>x. f`x,domain(f),A, r)"
+*)
+
+text\<open>A function is cofinal if it range is.\<close>
+definition
+  cofinal_fun :: "[i,i,i] \<Rightarrow> o" where
+  "cofinal_fun(f,A,r) \<equiv> \<forall>a\<in>A. \<exists>x\<in>domain(f). \<langle>a,f`x\<rangle>\<in>r \<or> a = f`x"
+
+lemma cofinal_funI:
+  assumes "\<And>a. a\<in>A \<Longrightarrow> \<exists>x\<in>domain(f). \<langle>a,f`x\<rangle>\<in>r \<or> a = f`x"
+  shows "cofinal_fun(f,A,r)"
+  using assms unfolding cofinal_fun_def by simp
+
+lemma cofinal_funD:
+  assumes "cofinal_fun(f,A,r)" "a\<in>A"
+  shows "\<exists>x\<in>domain(f). \<langle>a,f`x\<rangle>\<in>r \<or> a = f`x"
+  using assms unfolding cofinal_fun_def by simp
+
+lemma cofinal_in_cofinal:
+  assumes
+    "trans(r)" "cofinal(Y,X,r)" "cofinal(X,A,r)"
+  shows
+    "cofinal(Y,A,r)"
+  unfolding cofinal_def
+proof
+  fix a
+  assume "a\<in>A"
+  moreover from \<open>cofinal(X,A,r)\<close>
+  have "b\<in>A\<Longrightarrow>\<exists>x\<in>X. \<langle>b,x\<rangle>\<in>r \<or> b=x" for b
+    unfolding cofinal_def by simp
+  ultimately
+  obtain y where "y\<in>X" "\<langle>a,y\<rangle>\<in>r \<or> a=y" by auto
+  moreover from \<open>cofinal(Y,X,r)\<close>
+  have "c\<in>X\<Longrightarrow>\<exists>y\<in>Y. \<langle>c,y\<rangle>\<in>r \<or> c=y" for c
+    unfolding cofinal_def by simp
+  ultimately
+  obtain x where "x\<in>Y" "\<langle>y,x\<rangle>\<in>r \<or> y=x" by auto
+  with \<open>a\<in>A\<close> \<open>y\<in>X\<close> \<open>\<langle>a,y\<rangle>\<in>r \<or> a=y\<close> \<open>trans(r)\<close>
+  show "\<exists>x\<in>Y. \<langle>a,x\<rangle>\<in>r \<or> a=x" unfolding trans_def by auto
+qed
+
+lemma codomain_is_cofinal:
+  assumes "cofinal_fun(f,A,r)" "f:C \<rightarrow> D"
+  shows "cofinal(D,A,r)"
+  unfolding cofinal_def
+proof
+  fix b
+  assume "b \<in> A"
+  moreover from assms
+  have "a\<in>A \<Longrightarrow> \<exists>x\<in>domain(f). \<langle>a, f ` x\<rangle> \<in> r \<or> a = f`x" for a
+    unfolding cofinal_fun_def by simp
+  ultimately
+  obtain x where "x\<in>domain(f)" "\<langle>b, f ` x\<rangle> \<in> r \<or> b = f`x"
+    by blast
+  moreover from \<open>f:C \<rightarrow> D\<close>  \<open>x\<in>domain(f)\<close>
+  have "f`x\<in>D"
+    using domain_of_fun apply_rangeI by simp
+  ultimately
+  show  "\<exists>y\<in>D. \<langle>b, y\<rangle> \<in> r \<or> b = y" by auto
+qed
+
+lemma cofinal_range_iff_cofinal_fun:
+  assumes "function(f)"
+  shows "cofinal(range(f),A,r) \<longleftrightarrow> cofinal_fun(f,A,r)"
+  unfolding cofinal_fun_def
+proof (intro iffI ballI)
+  fix a
+  assume "a\<in>A" \<open>cofinal(range(f),A,r)\<close>
+  then
+  obtain y where "y\<in>range(f)" "\<langle>a,y\<rangle> \<in> r \<or> a = y"
+    unfolding cofinal_def by blast
+  moreover from this
+  obtain x where "\<langle>x,y\<rangle>\<in>f"
+    unfolding range_def domain_def converse_def by blast
+  moreover
+  note \<open>function(f)\<close>
+  ultimately
+  have "\<langle>a, f ` x\<rangle> \<in> r \<or> a = f ` x"
+    using function_apply_equality by blast
+  with \<open>\<langle>x,y\<rangle>\<in>f\<close>
+  show "\<exists>x\<in>domain(f). \<langle>a, f ` x\<rangle> \<in> r \<or> a = f ` x"  by blast
+next
+  assume "\<forall>a\<in>A. \<exists>x\<in>domain(f). \<langle>a, f ` x\<rangle> \<in> r \<or> a = f ` x"
+  with assms
+  show "cofinal(range(f), A, r)"
+    using function_apply_Pair[of f] unfolding cofinal_def by fast
+qed
+
+lemma cofinal_comp:
+  assumes
+    "f\<in> mono_map(C,s,D,r)" "cofinal_fun(f,D,r)" "h:B \<rightarrow> C"  "cofinal_fun(h,C,s)"
+    "trans(r)"
+  shows "cofinal_fun(f O h,D,r)"
+  unfolding cofinal_fun_def
+proof
+  fix a
+  from \<open>f\<in> mono_map(C,s,D,r)\<close>
+  have "f:C \<rightarrow> D"
+    using mono_map_is_fun by simp
+  with \<open>h:B \<rightarrow> C\<close>
+  have "domain(f) = C" "domain(h) = B"
+    using domain_of_fun by simp_all
+  moreover
+  assume "a \<in> D"
+  moreover
+  note \<open>cofinal_fun(f,D,r)\<close>
+  ultimately
+  obtain c where "c\<in>C"  "\<langle>a, f ` c\<rangle> \<in> r \<or> a = f ` c"
+    unfolding cofinal_fun_def by blast
+  with \<open>cofinal_fun(h,C,s)\<close> \<open>domain(h) = B\<close>
+  obtain b where "b \<in> B"  "\<langle>c, h ` b\<rangle> \<in> s \<or> c = h ` b"
+    unfolding cofinal_fun_def by blast
+  moreover from this and \<open>h:B \<rightarrow> C\<close>
+  have "h`b \<in> C" by simp
+  moreover
+  note \<open>f \<in> mono_map(C,s,D,r)\<close>  \<open>c\<in>C\<close>
+  ultimately
+  have "\<langle>f`c, f` (h ` b)\<rangle> \<in> r \<or> f`c = f` (h ` b)"
+    unfolding mono_map_def by blast
+  with \<open>\<langle>a, f ` c\<rangle> \<in> r \<or> a = f ` c\<close> \<open>trans(r)\<close> \<open>h:B \<rightarrow> C\<close> \<open>b\<in>B\<close>
+  have "\<langle>a, (f O h) ` b\<rangle> \<in> r \<or> a = (f O h) ` b"
+    using transD by auto
+  moreover from \<open>h:B \<rightarrow> C\<close> \<open>domain(f) = C\<close> \<open>domain(h) = B\<close>
+  have "domain(f O h) = B"
+    using range_fun_subset_codomain by blast
+  moreover
+  note \<open>b\<in>B\<close>
+  ultimately
+  show "\<exists>x\<in>domain(f O h). \<langle>a, (f O h) ` x\<rangle> \<in> r \<or> a = (f O h) ` x"  by blast
+qed
+
+definition
+  cf_fun :: "[i,i] \<Rightarrow> o" where
+  "cf_fun(f,\<alpha>) \<equiv> cofinal_fun(f,\<alpha>,Memrel(\<alpha>))"
+
+lemma cf_funI[intro!]: "cofinal_fun(f,\<alpha>,Memrel(\<alpha>)) \<Longrightarrow> cf_fun(f,\<alpha>)"
+  unfolding cf_fun_def by simp
+
+lemma cf_funD[dest!]: "cf_fun(f,\<alpha>) \<Longrightarrow> cofinal_fun(f,\<alpha>,Memrel(\<alpha>))"
+  unfolding cf_fun_def by simp
+
+lemma cf_fun_comp:
+  assumes
+    "Ord(\<alpha>)" "f\<in> mono_map(C,s,\<alpha>,Memrel(\<alpha>))" "cf_fun(f,\<alpha>)"
+    "h:B \<rightarrow> C" "cofinal_fun(h,C,s)"
+  shows "cf_fun(f O h,\<alpha>)"
+  using assms cofinal_comp[OF _ _ _ _ trans_Memrel] by auto
+
+definition
+  cf :: "i\<Rightarrow>i" where
+  "cf(\<gamma>) \<equiv> \<mu> \<beta>.  \<exists>A. A\<subseteq>\<gamma> \<and> cofinal(A,\<gamma>,Memrel(\<gamma>)) \<and> \<beta> = ordertype(A,Memrel(\<gamma>))"
+
+lemma Ord_cf [TC]: "Ord(cf(\<beta>))"
+  unfolding cf_def using Ord_Least by simp
+
+lemma gamma_cofinal_gamma:
+  assumes "Ord(\<gamma>)"
+  shows "cofinal(\<gamma>,\<gamma>,Memrel(\<gamma>))"
+  unfolding cofinal_def by auto
+
+lemma cf_is_ordertype:
+  assumes "Ord(\<gamma>)"
+  shows "\<exists>A. A\<subseteq>\<gamma> \<and> cofinal(A,\<gamma>,Memrel(\<gamma>)) \<and> cf(\<gamma>) = ordertype(A,Memrel(\<gamma>))"
+    (is "?P(cf(\<gamma>))")
+  using gamma_cofinal_gamma LeastI[of ?P \<gamma>] ordertype_Memrel[symmetric] assms
+  unfolding cf_def by blast
+
+lemma cf_fun_succ':
+  assumes "Ord(\<beta>)" "Ord(\<alpha>)" "f:\<alpha>\<rightarrow>succ(\<beta>)"
+  shows "(\<exists>x\<in>\<alpha>. f`x=\<beta>) \<longleftrightarrow> cf_fun(f,succ(\<beta>))"
+proof (intro iffI)
+  assume "(\<exists>x\<in>\<alpha>. f`x=\<beta>)"
+  with assms
+  show "cf_fun(f,succ(\<beta>))"
+    using domain_of_fun[OF \<open>f:\<alpha>\<rightarrow>succ(\<beta>)\<close>]
+    unfolding cf_fun_def cofinal_fun_def by auto
+next
+  assume "cf_fun(f,succ(\<beta>))"
+  with assms
+  obtain x where "x\<in>\<alpha>" "\<langle>\<beta>,f`x\<rangle> \<in> Memrel(succ(\<beta>)) \<or> \<beta> = f ` x"
+    using domain_of_fun[OF \<open>f:\<alpha>\<rightarrow>succ(\<beta>)\<close>]
+    unfolding cf_fun_def cofinal_fun_def by auto
+  moreover from \<open>Ord(\<beta>)\<close>
+  have "\<langle>\<beta>,y\<rangle> \<notin> Memrel(succ(\<beta>))" for y
+    using foundation unfolding Memrel_def by blast
+  ultimately
+  show "\<exists>x\<in>\<alpha>. f ` x = \<beta>" by blast
+qed
+
+lemma cf_fun_succ:
+  "Ord(\<beta>) \<Longrightarrow> f:1\<rightarrow>succ(\<beta>) \<Longrightarrow> f`0=\<beta> \<Longrightarrow> cf_fun(f,succ(\<beta>))"
+  using cf_fun_succ' by blast
+
+lemma ordertype_0_not_cofinal_succ:
+  assumes "ordertype(A,Memrel(succ(i))) = 0"  "A\<subseteq>succ(i)" "Ord(i)"
+  shows "\<not>cofinal(A,succ(i),Memrel(succ(i)))"
+proof
+  have 1:"ordertype(A,Memrel(succ(i))) = ordertype(0,Memrel(0))"
+    using \<open>ordertype(A,Memrel(succ(i))) = 0\<close> ordertype_0 by simp
+  from  \<open>A\<subseteq>succ(i)\<close> \<open>Ord(i)\<close>
+  have "\<exists>f. f \<in> \<langle>A, Memrel(succ(i))\<rangle> \<cong> \<langle>0, Memrel(0)\<rangle>"
+    using   well_ord_Memrel well_ord_subset
+      ordertype_eq_imp_ord_iso[OF 1] Ord_0  by blast
+  then
+  have "A=0"
+    using  ord_iso_is_bij bij_imp_eqpoll eqpoll_0_is_0 by blast
+  moreover
+  assume "cofinal(A, succ(i), Memrel(succ(i)))"
+  moreover
+  note \<open>Ord(i)\<close>
+  ultimately
+  show "False"
+    using not_mem_empty unfolding cofinal_def by auto
+qed
+
+text\<open>I thank Edwin Pacheco Rodríguez for the following lemma.\<close>
+lemma cf_succ:
+  assumes "Ord(\<alpha>)"
+  shows "cf(succ(\<alpha>)) = 1"
+proof -
+  define f where "f \<equiv> {\<langle>0,\<alpha>\<rangle>}"
+  then
+  have  "f : 1\<rightarrow>succ(\<alpha>)" "f`0 = \<alpha>"
+    using fun_extend3[of 0 0 "succ(\<alpha>)" 0 \<alpha>] singleton_0 by auto
+  with assms
+  have "cf_fun(f,succ(\<alpha>))"
+    using cf_fun_succ unfolding cofinal_fun_def by simp
+  from \<open>f:1\<rightarrow>succ(\<alpha>)\<close>
+  have "0\<in>domain(f)" using domain_of_fun by simp
+  define A where "A={f`0}"
+  with \<open>cf_fun(f,succ(\<alpha>))\<close> \<open>0\<in>domain(f)\<close> \<open>f`0=\<alpha>\<close>
+  have "cofinal(A,succ(\<alpha>),Memrel(succ(\<alpha>)))"
+    unfolding cofinal_def cofinal_fun_def by simp
+  moreover from  \<open>f`0=\<alpha>\<close> \<open>A={f`0}\<close>
+  have "A \<subseteq> succ(\<alpha>)" unfolding succ_def  by auto
+  moreover from \<open>Ord(\<alpha>)\<close> \<open>A\<subseteq> succ(\<alpha>)\<close>
+  have "well_ord(A,Memrel(succ(\<alpha>)))"
+    using Ord_succ well_ord_Memrel  well_ord_subset relation_Memrel by blast
+  moreover from \<open>Ord(\<alpha>)\<close>
+  have "\<not>(\<exists>A. A \<subseteq> succ(\<alpha>) \<and> cofinal(A, succ(\<alpha>), Memrel(succ(\<alpha>))) \<and> 0 = ordertype(A, Memrel(succ(\<alpha>))))"
+    (is "\<not>?P(0)")
+    using ordertype_0_not_cofinal_succ  unfolding cf_def  by auto
+  moreover
+  have "1 = ordertype(A,Memrel(succ(\<alpha>)))"
+  proof -
+    from \<open>A={f`0}\<close>
+    have "A\<approx>1" using singleton_eqpoll_1 by simp
+    with \<open>well_ord(A,Memrel(succ(\<alpha>)))\<close>
+    show ?thesis using nat_1I ordertype_eq_n by simp
+  qed
+  ultimately
+  show "cf(succ(\<alpha>)) = 1" using Ord_1  Least_equality[of ?P 1]
+    unfolding cf_def by blast
+qed
+
+lemma cf_zero [simp]:
+  "cf(0) = 0"
+  unfolding cf_def cofinal_def using
+    ordertype_0 subset_empty_iff Least_le[of _ 0] by auto
+
+lemma surj_is_cofinal: "f \<in> surj(\<delta>,\<gamma>) \<Longrightarrow> cf_fun(f,\<gamma>)"
+  unfolding surj_def cofinal_fun_def cf_fun_def
+  using domain_of_fun by force
+
+lemma cf_zero_iff: "Ord(\<alpha>) \<Longrightarrow> cf(\<alpha>) = 0 \<longleftrightarrow> \<alpha> = 0"
+proof (intro iffI)
+  assume "\<alpha> = 0" "Ord(\<alpha>)"
+  then
+  show "cf(\<alpha>) = 0" using cf_zero by simp
+next
+  assume "cf(\<alpha>) = 0" "Ord(\<alpha>)"
+  moreover from this
+  obtain A where "A\<subseteq>\<alpha>" "cf(\<alpha>) = ordertype(A,Memrel(\<alpha>))"
+    "cofinal(A,\<alpha>,Memrel(\<alpha>))"
+    using cf_is_ordertype by blast
+  ultimately
+  have "cofinal(0,\<alpha>,Memrel(\<alpha>))"
+    using ordertype_zero_imp_zero[of A "Memrel(\<alpha>)"] by simp
+  then
+  show "\<alpha>=0"
+    unfolding cofinal_def by blast
+qed
+
+\<comment> \<open>TODO: define Succ (predicate for successor ordinals)\<close>
+lemma cf_eq_one_iff:
+  assumes "Ord(\<gamma>)"
+  shows "cf(\<gamma>) = 1 \<longleftrightarrow> (\<exists>\<alpha>. Ord(\<alpha>) \<and> \<gamma>  = succ(\<alpha>))"
+proof (intro iffI)
+  assume "\<exists>\<alpha>. Ord(\<alpha>) \<and> \<gamma>  = succ(\<alpha>)"
+  then
+  show "cf(\<gamma>) = 1" using cf_succ by auto
+next
+  assume "cf(\<gamma>) = 1"
+  moreover from assms
+  obtain A where "A \<subseteq> \<gamma>" "cf(\<gamma>) = ordertype(A,Memrel(\<gamma>))"
+    "cofinal(A,\<gamma>,Memrel(\<gamma>))"
+    using cf_is_ordertype by blast
+  ultimately
+  have "ordertype(A,Memrel(\<gamma>)) = 1" by simp
+  moreover
+  define f where "f\<equiv>converse(ordermap(A,Memrel(\<gamma>)))"
+  moreover from this \<open>ordertype(A,Memrel(\<gamma>)) = 1\<close> \<open>A \<subseteq> \<gamma>\<close> assms
+  have "f \<in> surj(1,A)"
+    using well_ord_subset[OF well_ord_Memrel, THEN ordermap_bij,
+        THEN bij_converse_bij, of \<gamma> A] bij_is_surj
+    by simp
+  with \<open>cofinal(A,\<gamma>,Memrel(\<gamma>))\<close>
+  have "\<forall>a\<in>\<gamma>. \<langle>a, f`0\<rangle> \<in> Memrel(\<gamma>) \<or> a = f`0"
+    unfolding cofinal_def surj_def
+    by auto
+  with assms \<open>A \<subseteq> \<gamma>\<close> \<open>f \<in> surj(1,A)\<close>
+  show "\<exists>\<alpha>. Ord(\<alpha>) \<and> \<gamma>  = succ(\<alpha>)"
+    using Ord_has_max_imp_succ[of \<gamma> "f`0"]
+      surj_is_fun[of f 1 A] apply_type[of f 1 "\<lambda>_.A" 0]
+    unfolding lt_def
+    by (auto intro:Ord_in_Ord)
+qed
+
+lemma ordertype_in_cf_imp_not_cofinal:
+  assumes
+    "ordertype(A,Memrel(\<gamma>)) \<in> cf(\<gamma>)"
+    "A \<subseteq> \<gamma>"
+  shows
+    "\<not> cofinal(A,\<gamma>,Memrel(\<gamma>))"
+proof
+  note \<open>A \<subseteq> \<gamma>\<close>
+  moreover
+  assume "cofinal(A,\<gamma>,Memrel(\<gamma>))"
+  ultimately
+  have "\<exists>B. B \<subseteq> \<gamma> \<and> cofinal(B, \<gamma>, Memrel(\<gamma>)) \<and>  ordertype(A,Memrel(\<gamma>)) = ordertype(B, Memrel(\<gamma>))"
+    (is "?P(ordertype(A,_))")
+    by blast
+  moreover from assms
+  have "ordertype(A,Memrel(\<gamma>)) < cf(\<gamma>)"
+    using Ord_cf ltI by blast
+  ultimately
+  show "False"
+    unfolding cf_def using less_LeastE[of ?P  "ordertype(A,Memrel(\<gamma>))"]
+    by auto
+qed
+
+lemma cofinal_mono_map_cf:
+  assumes "Ord(\<gamma>)"
+  shows "\<exists>j \<in> mono_map(cf(\<gamma>), Memrel(cf(\<gamma>)), \<gamma>, Memrel(\<gamma>)) . cf_fun(j,\<gamma>)"
+proof -
+  note assms
+  moreover from this
+  obtain A where "A \<subseteq> \<gamma>" "cf(\<gamma>) = ordertype(A,Memrel(\<gamma>))"
+    "cofinal(A,\<gamma>,Memrel(\<gamma>))"
+    using cf_is_ordertype by blast
+  moreover
+  define j where "j \<equiv> converse(ordermap(A,Memrel(\<gamma>)))"
+  moreover from calculation
+  have "j :cf(\<gamma>) \<rightarrow>\<^sub>< \<gamma>"
+    using ordertype_ord_iso[THEN ord_iso_sym,
+        THEN ord_iso_is_mono_map, THEN mono_map_mono,
+        of A "Memrel(\<gamma>)" \<gamma>] well_ord_Memrel[THEN well_ord_subset]
+    by simp
+  moreover from calculation
+  have "j \<in> surj(cf(\<gamma>),A)"
+    using well_ord_Memrel[THEN well_ord_subset, THEN ordertype_ord_iso,
+        THEN ord_iso_sym, of \<gamma> A, THEN ord_iso_is_bij,
+        THEN bij_is_surj]
+    by simp
+  with \<open>cofinal(A,\<gamma>,Memrel(\<gamma>))\<close>
+  have "cf_fun(j,\<gamma>)"
+    using cofinal_range_iff_cofinal_fun[of j \<gamma> "Memrel(\<gamma>)"]
+      surj_range[of j "cf(\<gamma>)" A] surj_is_fun fun_is_function
+    by fastforce
+  with \<open>j \<in> mono_map(_,_,_,_)\<close>
+  show ?thesis by auto
+qed
+
+
+subsection\<open>The factorization lemma\<close>
+
+text\<open>In this subsection we prove a factorization lemma for cofinal functions
+into ordinals, which shows that any cofinal function between ordinals can be
+“decomposed” in such a way that a commutative triangle of strictly increasing
+maps arises.
+
+The factorization lemma has a kind of
+fundamental character, in that the rest of the basic results on cofinality
+(for, instance, idempotence) follow easily from it, in a more algebraic way.
+
+This is a consequence that the proof encapsulates uses of transfinite
+recursion in the basic theory of cofinality; indeed, only one use is needed.
+In the setting of Isabelle/ZF, this is convenient since the machinery of
+recursion is pretty clumsy. On the downside, this way of presenting things 
+results in a longer proof of the factorization lemma. This approach was
+taken by the author in the notes \cite{apunte_st} for an introductory course
+in Set Theory.
+
+To organize the use of the hypotheses of the factorization lemma,
+we set up a locale containing all the relevant ingredients.
+\<close>
+locale cofinal_factor =
+  fixes j \<delta> \<xi> \<gamma> f
+  assumes j_mono: "j :\<xi> \<rightarrow>\<^sub>< \<gamma>"
+    and     ords: "Ord(\<delta>)" "Ord(\<xi>)" "Limit(\<gamma>)"
+    and   f_type: "f: \<delta> \<rightarrow> \<gamma>"
+begin
+
+text\<open>Here, \<^term>\<open>f\<close> is cofinal function from \<^term>\<open>\<delta>\<close> to \<^term>\<open>\<gamma>\<close>, and the
+ordinal \<^term>\<open>\<xi>\<close> is meant to be the cofinality of \<^term>\<open>\<gamma>\<close>. Hence, there exists
+an increasing map \<^term>\<open>j\<close> from  \<^term>\<open>\<xi>\<close> to  \<^term>\<open>\<gamma>\<close> by the last lemma.
+
+The main goal is to construct an increasing function \<^term>\<open>g:\<xi>\<rightarrow>\<delta>\<close> such that
+the composition \<^term>\<open>f O g\<close> is still cofinal but also increasing.\<close>
+
+definition
+  factor_body :: "[i,i,i] \<Rightarrow> o" where
+  "factor_body(\<beta>,h,x) \<equiv> (x\<in>\<delta> \<and> j`\<beta> \<le> f`x \<and> (\<forall>\<alpha><\<beta> . f`(h`\<alpha>) < f`x)) \<or> x=\<delta>"
+
+definition
+  factor_rec :: "[i,i] \<Rightarrow> i" where
+  "factor_rec(\<beta>,h) \<equiv>  \<mu> x. factor_body(\<beta>,h,x)"
+
+txt\<open>\<^term>\<open>factor_rec\<close> is the inductive step for the definition by transfinite
+recursion of the \<^emph>\<open>factor\<close> function (called \<^term>\<open>g\<close> above), which in
+turn is obtained by minimizing the predicate \<^term>\<open>factor_body\<close>. Next we show
+that this predicate is monotonous.\<close>
+
+lemma factor_body_mono:
+  assumes
+    "\<beta>\<in>\<xi>" "\<alpha><\<beta>"
+    "factor_body(\<beta>,\<lambda>x\<in>\<beta>. G(x),x)"
+  shows
+    "factor_body(\<alpha>,\<lambda>x\<in>\<alpha>. G(x),x)"
+proof -
+  from \<open>\<alpha><\<beta>\<close>
+  have "\<alpha>\<in>\<beta>" using ltD by simp
+  moreover
+  note \<open>\<beta>\<in>\<xi>\<close>
+  moreover from calculation
+  have "\<alpha>\<in>\<xi>" using ords ltD Ord_cf Ord_trans by blast
+  ultimately
+  have "j`\<alpha> \<in> j`\<beta>" using j_mono mono_map_increasing by blast
+  moreover from \<open>\<beta>\<in>\<xi>\<close>
+  have "j`\<beta>\<in>\<gamma>"
+    using j_mono domain_of_fun apply_rangeI mono_map_is_fun by force
+  moreover from this
+  have "Ord(j`\<beta>)"
+    using Ord_in_Ord ords Limit_is_Ord by auto
+  ultimately
+  have "j`\<alpha> \<le> j`\<beta>"  unfolding lt_def by blast
+  then
+  have "j`\<beta> \<le> f`\<theta> \<Longrightarrow> j`\<alpha> \<le> f`\<theta>" for \<theta> using le_trans by blast
+  moreover
+  have "f`((\<lambda>w\<in>\<alpha>. G(w))`y) < f`z" if "z\<in>\<delta>" "\<forall>x<\<beta>. f`((\<lambda>w\<in>\<beta>. G(w))`x) < f`z" "y<\<alpha>" for y z
+  proof -
+    note \<open>y<\<alpha>\<close>
+    also
+    note \<open>\<alpha><\<beta>\<close>
+    finally
+    have "y<\<beta>" by simp
+    with \<open>\<forall>x<\<beta>. f`((\<lambda>w\<in>\<beta>. G(w))`x) < f`z\<close>
+    have "f ` ((\<lambda>w\<in>\<beta>. G(w)) ` y) < f ` z" by simp
+    moreover from \<open>y<\<alpha>\<close> \<open>y<\<beta>\<close>
+    have "(\<lambda>w\<in>\<beta>. G(w)) ` y = (\<lambda>w\<in>\<alpha>. G(w)) ` y"
+      using beta_if  by (auto dest:ltD)
+    ultimately show ?thesis by simp
+  qed
+  moreover
+  note \<open>factor_body(\<beta>,\<lambda>x\<in>\<beta>. G(x),x)\<close>
+  ultimately
+  show ?thesis
+    unfolding factor_body_def by blast
+qed
+
+lemma factor_body_simp[simp]: "factor_body(\<alpha>,g,\<delta>)"
+  unfolding factor_body_def by simp
+
+lemma factor_rec_mono:
+  assumes
+    "\<beta>\<in>\<xi>" "\<alpha><\<beta>"
+  shows
+    "factor_rec(\<alpha>,\<lambda>x\<in>\<alpha>. G(x)) \<le> factor_rec(\<beta>,\<lambda>x\<in>\<beta>. G(x))"
+  unfolding factor_rec_def
+  using assms ords factor_body_mono Least_antitone by simp
+
+text\<open>We now define the factor as higher-order function.
+Later it will be restricted to a set to obtain a bona fide function of
+type @{typ i}.\<close>
+definition
+  factor :: "i \<Rightarrow> i" where
+  "factor(\<beta>) \<equiv> transrec(\<beta>,factor_rec)"
+
+lemma factor_unfold:
+  "factor(\<alpha>) = factor_rec(\<alpha>,\<lambda>x\<in>\<alpha>. factor(x))"
+  using def_transrec[OF factor_def] .
+
+lemma factor_mono:
+  assumes "\<beta>\<in>\<xi>" "\<alpha><\<beta>" "factor(\<alpha>)\<noteq>\<delta>" "factor(\<beta>)\<noteq>\<delta>"
+  shows "factor(\<alpha>) \<le> factor(\<beta>)"
+proof -
+  have "factor(\<alpha>) = factor_rec(\<alpha>, \<lambda>x\<in>\<alpha>. factor(x))"
+    using factor_unfold .
+  also from assms and factor_rec_mono
+  have "... \<le> factor_rec(\<beta>, \<lambda>x\<in>\<beta>. factor(x))"
+    by simp
+  also
+  have "factor_rec(\<beta>, \<lambda>x\<in>\<beta>. factor(x)) = factor(\<beta>)"
+    using def_transrec[OF factor_def, symmetric] .
+  finally show ?thesis .
+qed
+
+text\<open>The factor satisfies the predicate body of the minimization.\<close>
+
+lemma factor_body_factor:
+  "factor_body(\<alpha>,\<lambda>x\<in>\<alpha>. factor(x),factor(\<alpha>))"
+  using ords factor_unfold[of \<alpha>]
+    LeastI[of "factor_body(_,_)" \<delta>]
+  unfolding factor_rec_def by simp
+
+lemma factor_type [TC]: "Ord(factor(\<alpha>))"
+  using ords factor_unfold[of \<alpha>]
+  unfolding factor_rec_def by simp
+
+text\<open>The value \<^term>\<open>\<delta>\<close> in \<^term>\<open>factor_body\<close> (and therefore, in
+\<^term>\<open>factor\<close>) is meant to be a “default value”. Whenever it is not 
+attained, the factor function behaves as expected: It is increasing
+and its composition with \<^term>\<open>f\<close> also is.\<close>
+
+lemma f_factor_increasing:
+  assumes "\<beta>\<in>\<xi>" "\<alpha><\<beta>" "factor(\<beta>)\<noteq>\<delta>"
+  shows "f`factor(\<alpha>) < f`factor(\<beta>)"
+proof -
+  from assms
+  have "f ` ((\<lambda>x\<in>\<beta>. factor(x)) ` \<alpha>) < f ` factor(\<beta>)"
+    using factor_unfold[of \<beta>] ords LeastI[of "factor_body(\<beta>,\<lambda>x\<in>\<beta>. factor(x))"]
+    unfolding factor_rec_def factor_body_def
+    by (auto simp del:beta_if)
+  with \<open>\<alpha><\<beta>\<close>
+  show ?thesis using ltD by auto
+qed
+
+lemma factor_increasing:
+  assumes "\<beta>\<in>\<xi>" "\<alpha><\<beta>" "factor(\<alpha>)\<noteq>\<delta>" "factor(\<beta>)\<noteq>\<delta>"
+  shows "factor(\<alpha>)<factor(\<beta>)"
+  using assms f_factor_increasing factor_mono by (force intro:le_neq_imp_lt)
+
+lemma factor_in_delta:
+  assumes "factor(\<beta>) \<noteq> \<delta>"
+  shows "factor(\<beta>) \<in> \<delta>"
+  using assms factor_body_factor ords
+  unfolding factor_body_def by auto
+
+text\<open>Finally, we define the (set) factor function as the restriction of
+factor to the ordinal  \<^term>\<open>\<xi>\<close>.\<close>
+
+definition
+  fun_factor :: "i" where
+  "fun_factor \<equiv> \<lambda>\<beta>\<in>\<xi>. factor(\<beta>)"
+
+lemma fun_factor_is_mono_map:
+  assumes "\<And>\<beta>. \<beta> \<in> \<xi> \<Longrightarrow> factor(\<beta>) \<noteq> \<delta>"
+  shows "fun_factor \<in> mono_map(\<xi>, Memrel(\<xi>), \<delta>, Memrel(\<delta>))"
+  unfolding mono_map_def
+proof (intro CollectI ballI impI)
+  (* Proof that \<^term>\<open>fun_factor\<close> respects membership *)
+  fix \<alpha> \<beta>
+  assume "\<alpha>\<in>\<xi>" "\<beta>\<in>\<xi>"
+  moreover
+  note assms
+  moreover from calculation
+  have "factor(\<alpha>)\<noteq>\<delta>" "factor(\<beta>)\<noteq>\<delta>" "Ord(\<beta>)"
+    using factor_in_delta Ord_in_Ord ords by auto
+  moreover
+  assume "\<langle>\<alpha>, \<beta>\<rangle> \<in> Memrel(\<xi>)"
+  ultimately
+  show "\<langle>fun_factor ` \<alpha>, fun_factor ` \<beta>\<rangle> \<in> Memrel(\<delta>)"
+    unfolding fun_factor_def
+    using ltI factor_increasing[THEN ltD] factor_in_delta
+    by simp
+next
+  (* Proof of type *)
+  from assms
+  show "fun_factor : \<xi> \<rightarrow> \<delta>"
+    unfolding fun_factor_def
+    using ltI lam_type factor_in_delta by simp
+qed
+
+lemma f_fun_factor_is_mono_map:
+  assumes "\<And>\<beta>. \<beta> \<in> \<xi> \<Longrightarrow> factor(\<beta>) \<noteq> \<delta>"
+  shows "f O fun_factor \<in> mono_map(\<xi>, Memrel(\<xi>), \<gamma>, Memrel(\<gamma>))"
+  unfolding mono_map_def
+  using f_type
+proof (intro CollectI ballI impI comp_fun[of _ _ \<delta>])
+  from assms
+  show "fun_factor : \<xi> \<rightarrow> \<delta>"
+    using fun_factor_is_mono_map mono_map_is_fun by simp
+      (* Proof that f O ?g respects membership *)
+  fix \<alpha> \<beta>
+  assume "\<langle>\<alpha>, \<beta>\<rangle> \<in> Memrel(\<xi>)"
+  then
+  have "\<alpha><\<beta>"
+    using Ord_in_Ord[of "\<xi>"] ltI ords by blast
+  assume "\<alpha>\<in>\<xi>" "\<beta>\<in>\<xi>"
+  moreover from this and assms
+  have "factor(\<alpha>)\<noteq>\<delta>" "factor(\<beta>)\<noteq>\<delta>" by auto
+  moreover
+  have "Ord(\<gamma>)" "\<gamma>\<noteq>0" using ords Limit_is_Ord by auto
+  moreover
+  note \<open>\<alpha><\<beta>\<close> \<open>fun_factor : \<xi> \<rightarrow> \<delta>\<close>
+  ultimately
+  show "\<langle>(f O fun_factor) ` \<alpha>, (f O fun_factor) ` \<beta>\<rangle> \<in> Memrel(\<gamma>)"
+    using ltD[of "f ` factor(\<alpha>)" "f ` factor(\<beta>)"]
+      f_factor_increasing apply_in_range f_type
+    unfolding fun_factor_def by auto
+qed
+
+end (* cofinal_factor *)
+
+text\<open>We state next the factorization lemma.\<close>
+
+lemma cofinal_fun_factorization:
+  notes le_imp_subset [dest] lt_trans2 [trans]
+  assumes
+    "Ord(\<delta>)" "Limit(\<gamma>)" "f: \<delta> \<rightarrow> \<gamma>" "cf_fun(f,\<gamma>)"
+  shows
+    "\<exists>g \<in> cf(\<gamma>) \<rightarrow>\<^sub>< \<delta>.  f O g : cf(\<gamma>) \<rightarrow>\<^sub>< \<gamma> \<and>
+           cofinal_fun(f O g,\<gamma>,Memrel(\<gamma>))"
+proof -
+  from \<open>Limit(\<gamma>)\<close>
+  have "Ord(\<gamma>)" using Limit_is_Ord by simp
+  then
+  obtain j where "j :cf(\<gamma>) \<rightarrow>\<^sub>< \<gamma>" "cf_fun(j,\<gamma>)"
+    using cofinal_mono_map_cf by blast
+  then
+  have "domain(j) = cf(\<gamma>)"
+    using domain_of_fun mono_map_is_fun by force
+  from \<open>j \<in> _\<close> assms
+  interpret cofinal_factor j \<delta> "cf(\<gamma>)"
+    by (unfold_locales) (simp_all)
+  text\<open>The core of the argument is to show that the factor function
+  indeed maps into \<^term>\<open>\<delta>\<close>, therefore its values satisfy the first
+  disjunct of \<^term>\<open>factor_body\<close>. This holds in turn because no
+  restriction of the factor composed with \<^term>\<open>f\<close> to a proper initial
+  segment of \<^term>\<open>cf(\<gamma>)\<close> can be cofinal in \<^term>\<open>\<gamma>\<close> by definition of
+  cofinality. Hence there must be a witness that satisfies the first
+  disjunct.\<close>
+  have factor_not_delta: "factor(\<beta>)\<noteq>\<delta>" if "\<beta> \<in> cf(\<gamma>)" for \<beta>
+    text\<open>For this, we induct on \<^term>\<open>\<beta>\<close> ranging over \<^term>\<open>cf(\<gamma>)\<close>.\<close>
+  proof (induct \<beta> rule:Ord_induct[OF _ Ord_cf[of \<gamma>]])
+    case 1 with that show ?case .
+  next
+    case (2 \<beta>)
+    then
+    have IH: "z\<in>\<beta> \<Longrightarrow> factor(z)\<noteq>\<delta>" for z by simp
+    define h where "h \<equiv> \<lambda>x\<in>\<beta>. f`factor(x)"
+    from IH
+    have "z\<in>\<beta> \<Longrightarrow> factor(z) \<in> \<delta>" for z
+      using factor_in_delta by blast
+    with \<open>f:\<delta>\<rightarrow>\<gamma>\<close>
+    have "h : \<beta> \<rightarrow> \<gamma>" unfolding h_def using apply_funtype lam_type by auto
+    then
+    have "h : \<beta> \<rightarrow>\<^sub>< \<gamma>"
+      unfolding mono_map_def
+    proof (intro CollectI ballI impI)
+      fix x y
+      assume "x\<in>\<beta>" "y\<in>\<beta>"
+      moreover from this and IH
+      have "factor(y) \<noteq> \<delta>" by simp
+      moreover from calculation and \<open>h \<in> \<beta> \<rightarrow> \<gamma>\<close>
+      have "h`x \<in> \<gamma>" "h`y \<in> \<gamma>" by simp_all
+      moreover from \<open>\<beta>\<in>cf(\<gamma>)\<close> and \<open>y\<in>\<beta>\<close>
+      have "y \<in> cf(\<gamma>)"
+        using Ord_trans Ord_cf by blast
+      moreover from this
+      have "Ord(y)"
+        using Ord_cf Ord_in_Ord by blast
+      moreover
+      assume "\<langle>x,y\<rangle> \<in> Memrel(\<beta>)"
+      moreover from calculation
+      have "x<y" by (blast intro:ltI)
+      ultimately
+      show "\<langle>h ` x, h ` y\<rangle> \<in> Memrel(\<gamma>)"
+        unfolding h_def using f_factor_increasing ltD by (auto)
+    qed
+    with \<open>\<beta>\<in>cf(\<gamma>)\<close> \<open>Ord(\<gamma>)\<close>
+    have "ordertype(h``\<beta>,Memrel(\<gamma>)) = \<beta>" (* Maybe should use range(h) *)
+      using mono_map_ordertype_image[of \<beta>] Ord_cf Ord_in_Ord by blast
+    also
+    note \<open>\<beta> \<in>cf(\<gamma>)\<close>
+    finally
+    have "ordertype(h``\<beta>,Memrel(\<gamma>)) \<in> cf(\<gamma>)" by simp
+    moreover from \<open>h \<in> \<beta> \<rightarrow> \<gamma>\<close>
+    have "h``\<beta> \<subseteq> \<gamma>"
+      using mono_map_is_fun Image_sub_codomain by blast
+    ultimately
+    have "\<not> cofinal(h``\<beta>,\<gamma>,Memrel(\<gamma>))"
+      using ordertype_in_cf_imp_not_cofinal by simp
+    then
+    obtain \<alpha>_0 where "\<alpha>_0\<in>\<gamma>" "\<forall>x\<in>h `` \<beta>. \<not> \<langle>\<alpha>_0, x\<rangle> \<in> Memrel(\<gamma>) \<and> \<alpha>_0 \<noteq> x"
+      unfolding cofinal_def by auto
+    with \<open>Ord(\<gamma>)\<close> \<open>h``\<beta> \<subseteq> \<gamma>\<close>
+    have "\<forall>x\<in>h `` \<beta>. x \<in> \<alpha>_0"
+      using well_ord_Memrel[of \<gamma>] well_ord_is_linear[of \<gamma> "Memrel(\<gamma>)"]
+      unfolding linear_def by blast
+    from \<open>\<alpha>_0 \<in> \<gamma>\<close> \<open>j \<in> mono_map(_,_,\<gamma>,_)\<close> \<open>Ord(\<gamma>)\<close>
+    have "j`\<beta> \<in> \<gamma>"
+      using mono_map_is_fun apply_in_range by force
+    with \<open>\<alpha>_0 \<in> \<gamma>\<close> \<open>Ord(\<gamma>)\<close>
+    have "\<alpha>_0 \<union> j`\<beta> \<in> \<gamma>"
+      using Un_least_mem_iff Ord_in_Ord by auto
+    with \<open>cf_fun(f,\<gamma>)\<close>
+    obtain \<theta> where "\<theta>\<in>domain(f)" "\<langle>\<alpha>_0 \<union> j`\<beta>, f ` \<theta>\<rangle> \<in> Memrel(\<gamma>) \<or>  \<alpha>_0 \<union> j`\<beta> = f ` \<theta>"
+      by (auto simp add:cofinal_fun_def) blast
+    moreover from this and \<open>f:\<delta>\<rightarrow>\<gamma>\<close>
+    have "\<theta> \<in> \<delta>" using domain_of_fun by auto
+    moreover
+    note \<open>Ord(\<gamma>)\<close>
+    moreover from this and \<open>f:\<delta>\<rightarrow>\<gamma>\<close>  \<open>\<alpha>_0 \<in> \<gamma>\<close>
+    have "Ord(f`\<theta>)"
+      using apply_in_range Ord_in_Ord by blast
+    moreover from calculation and \<open>\<alpha>_0 \<in> \<gamma>\<close> and \<open>Ord(\<delta>)\<close> and \<open>j`\<beta> \<in> \<gamma>\<close>
+    have "Ord(\<alpha>_0)" "Ord(j`\<beta>)" "Ord(\<theta>)"
+      using Ord_in_Ord by auto
+    moreover from \<open>\<forall>x\<in>h `` \<beta>. x \<in> \<alpha>_0\<close> \<open>Ord(\<alpha>_0)\<close> \<open>h:\<beta>\<rightarrow>\<gamma>\<close>
+    have "x\<in>\<beta> \<Longrightarrow> h`x < \<alpha>_0" for x
+      using fun_is_function[of h \<beta> "\<lambda>_. \<gamma>"]
+        Image_subset_Ord_imp_lt domain_of_fun[of h \<beta> "\<lambda>_. \<gamma>"]
+      by blast
+    moreover
+    have "x\<in>\<beta> \<Longrightarrow> h`x < f`\<theta>" for x
+    proof -
+      fix x
+      assume "x\<in>\<beta>"
+      with \<open>\<forall>x\<in>h `` \<beta>. x \<in> \<alpha>_0\<close> \<open>Ord(\<alpha>_0)\<close> \<open>h:\<beta>\<rightarrow>\<gamma>\<close>
+      have "h`x < \<alpha>_0"
+        using fun_is_function[of h \<beta> "\<lambda>_. \<gamma>"]
+          Image_subset_Ord_imp_lt domain_of_fun[of h \<beta> "\<lambda>_. \<gamma>"]
+        by blast
+      also from \<open>\<langle>\<alpha>_0 \<union> _, f ` \<theta>\<rangle> \<in> Memrel(\<gamma>) \<or> \<alpha>_0 \<union> _= f ` \<theta>\<close>
+        \<open>Ord(f`\<theta>)\<close> \<open>Ord(\<alpha>_0)\<close> \<open>Ord(j`\<beta>)\<close>
+      have "\<alpha>_0 \<le> f`\<theta>"
+        using Un_leD1[OF leI [OF ltI]] Un_leD1[OF le_eqI] by blast
+      finally
+      show "h`x < f`\<theta>" .
+    qed
+    ultimately
+    have "factor_body(\<beta>,\<lambda>x\<in>\<beta>. factor(x),\<theta>)"
+      unfolding h_def factor_body_def using ltD
+      by (auto dest:Un_memD2 Un_leD2[OF le_eqI])
+    with \<open>Ord(\<theta>)\<close>
+    have "factor(\<beta>) \<le> \<theta>"
+      using factor_unfold[of \<beta>] Least_le unfolding factor_rec_def by auto
+    with \<open>\<theta>\<in>\<delta>\<close> \<open>Ord(\<delta>)\<close>
+    have "factor(\<beta>) \<in> \<delta>"
+      using leI[of \<theta>] ltI[of \<theta>]  by (auto dest:ltD)
+    then
+    show ?case by (auto elim:mem_irrefl)
+  qed
+  moreover
+  have "cofinal_fun(f O fun_factor, \<gamma>, Memrel(\<gamma>))"
+  proof (intro cofinal_funI)
+    fix a
+    assume "a \<in> \<gamma>"
+    with \<open>cf_fun(j,\<gamma>)\<close> \<open>domain(j) = cf(\<gamma>)\<close>
+    obtain x where "x\<in>cf(\<gamma>)" "a \<in> j`x \<or> a = j`x"
+      by (auto simp add:cofinal_fun_def) blast
+    with factor_not_delta
+    have "x \<in> domain(f O fun_factor)"
+      using f_fun_factor_is_mono_map mono_map_is_fun domain_of_fun by force
+    moreover
+    have "a \<in> (f O fun_factor) `x \<or> a = (f O fun_factor) `x"
+    proof -
+      from \<open>x\<in>cf(\<gamma>)\<close> factor_not_delta
+      have "j ` x \<le> f ` factor(x)"
+        using mem_not_refl factor_body_factor factor_in_delta
+        unfolding factor_body_def by auto
+      with \<open>a \<in> j`x \<or> a = j`x\<close>
+      have "a \<in> f ` factor(x) \<or> a = f ` factor(x)"
+        using ltD by blast
+      with \<open>x\<in>cf(\<gamma>)\<close>
+      show ?thesis using lam_funtype[of "cf(\<gamma>)" factor]
+        unfolding fun_factor_def by auto
+    qed
+    moreover
+    note \<open>a \<in> \<gamma>\<close>
+    moreover from calculation and \<open>Ord(\<gamma>)\<close> and factor_not_delta
+    have "(f O fun_factor) `x \<in> \<gamma>"
+      using Limit_nonzero apply_in_range mono_map_is_fun[of "f O fun_factor"]
+        f_fun_factor_is_mono_map by blast
+    ultimately
+    show "\<exists>x \<in> domain(f O fun_factor). \<langle>a, (f O fun_factor) ` x\<rangle> \<in> Memrel(\<gamma>)
+                                       \<or> a = (f O fun_factor) `x"
+      by blast
+  qed
+  ultimately
+  show ?thesis
+    using fun_factor_is_mono_map f_fun_factor_is_mono_map by blast
+qed
+
+text\<open>As a final observation in this part, we note that if the original
+cofinal map was increasing, then the factor function is also cofinal.\<close>
+lemma factor_is_cofinal:
+  assumes
+    "Ord(\<delta>)" "Ord(\<gamma>)"
+    "f :\<delta> \<rightarrow>\<^sub>< \<gamma>"  "f O g \<in> mono_map(\<alpha>,r,\<gamma>,Memrel(\<gamma>))"
+    "cofinal_fun(f O g,\<gamma>,Memrel(\<gamma>))" "g: \<alpha> \<rightarrow> \<delta>"
+  shows
+    "cf_fun(g,\<delta>)"
+  unfolding cf_fun_def cofinal_fun_def
+proof
+  fix a
+  assume "a \<in> \<delta>"
+  with \<open>f \<in> mono_map(\<delta>,_,\<gamma>,_)\<close>
+  have "f`a \<in> \<gamma>"
+    using mono_map_is_fun by force
+  with \<open>cofinal_fun(f O g,\<gamma>,_)\<close>
+  obtain y where "y\<in>\<alpha>"  "\<langle>f`a, (f O g) ` y\<rangle> \<in> Memrel(\<gamma>) \<or> f`a = (f O g) ` y"
+    unfolding cofinal_fun_def using domain_of_fun[OF \<open>g:\<alpha> \<rightarrow> \<delta>\<close>] by blast
+  with \<open>g:\<alpha> \<rightarrow> \<delta>\<close>
+  have "\<langle>f`a, f ` (g ` y)\<rangle> \<in> Memrel(\<gamma>) \<or> f`a = f ` (g ` y)" "g`y \<in> \<delta>"
+    using comp_fun_apply[of g \<alpha> \<delta> y f] by auto
+  with assms(1-3) and \<open>a\<in>\<delta>\<close>
+  have "\<langle>a, g ` y\<rangle> \<in> Memrel(\<delta>) \<or> a = g ` y"
+    using Memrel_mono_map_reflects Memrel_mono_map_is_inj[of \<delta> f \<gamma> \<gamma>]
+      inj_apply_equality[of f \<delta> \<gamma>]  by blast
+  with \<open>y\<in>\<alpha>\<close>
+  show "\<exists>x\<in>domain(g). \<langle>a, g ` x\<rangle> \<in> Memrel(\<delta>) \<or> a = g ` x"
+    using domain_of_fun[OF \<open>g:\<alpha> \<rightarrow> \<delta>\<close>] by blast
+qed
+
+
+subsection\<open>Classical results on cofinalities\<close>
+
+text\<open>Now the rest of the results follow in a more algebraic way. The
+next proof one invokes a case analysis on whether the argument is zero,
+a successor ordinal or a limit one; the last case being the most
+relevant one and is immediate from the factorization lemma.\<close>
+
+lemma cf_le_domain_cofinal_fun:
+  assumes
+    "Ord(\<gamma>)" "Ord(\<delta>)" "f:\<delta> \<rightarrow> \<gamma>" "cf_fun(f,\<gamma>)"
+  shows
+    "cf(\<gamma>)\<le>\<delta>"
+  using assms
+proof (cases rule:Ord_cases)
+  case 0
+  with \<open>Ord(\<delta>)\<close>
+  show ?thesis using Ord_0_le by simp
+next
+  case (succ \<gamma>)
+  with assms
+  obtain x where "x\<in>\<delta>" "f`x=\<gamma>" using cf_fun_succ' by blast
+  then
+  have "\<delta>\<noteq>0" by blast
+  let ?f="{\<langle>0,f`x\<rangle>}"
+  from \<open>f`x=\<gamma>\<close>
+  have "?f:1\<rightarrow>succ(\<gamma>)"
+    using singleton_0 singleton_fun[of 0 \<gamma>] singleton_subsetI fun_weaken_type by simp
+  with \<open>Ord(\<gamma>)\<close>  \<open>f`x=\<gamma>\<close>
+  have "cf(succ(\<gamma>)) = 1" using cf_succ by simp
+  with \<open>\<delta>\<noteq>0\<close> succ
+  show ?thesis using Ord_0_lt_iff succ_leI \<open>Ord(\<delta>)\<close> by simp
+next
+  case (limit)
+  with assms
+  obtain g where "g :cf(\<gamma>) \<rightarrow>\<^sub>< \<delta>"
+    using cofinal_fun_factorization by blast
+  with assms
+  show ?thesis using mono_map_imp_le by simp
+qed
+
+lemma cf_ordertype_cofinal:
+  assumes
+    "Limit(\<gamma>)" "A\<subseteq>\<gamma>" "cofinal(A,\<gamma>,Memrel(\<gamma>))"
+  shows
+    "cf(\<gamma>) = cf(ordertype(A,Memrel(\<gamma>)))"
+proof (intro le_anti_sym)
+  from \<open>Limit(\<gamma>)\<close>
+  have "Ord(\<gamma>)"
+    using Limit_is_Ord by simp
+  with \<open>A \<subseteq> \<gamma>\<close>
+  have "well_ord(A,Memrel(\<gamma>))"
+    using well_ord_Memrel well_ord_subset by blast
+  then
+  obtain f \<alpha> where "f:\<langle>\<alpha>, Memrel(\<alpha>)\<rangle> \<cong> \<langle>A,Memrel(\<gamma>)\<rangle>" "Ord(\<alpha>)" "\<alpha> = ordertype(A,Memrel(\<gamma>))"
+    using ordertype_ord_iso Ord_ordertype ord_iso_sym by blast
+  moreover from this
+  have "f: \<alpha> \<rightarrow> A"
+    using ord_iso_is_mono_map mono_map_is_fun[of f _ "Memrel(\<alpha>)"] by blast
+  moreover from this
+  have "function(f)"
+    using fun_is_function by simp
+  moreover from \<open>f:\<langle>\<alpha>, Memrel(\<alpha>)\<rangle> \<cong> \<langle>A,Memrel(\<gamma>)\<rangle>\<close>
+  have "range(f) = A"
+    using ord_iso_is_bij bij_is_surj surj_range by blast
+  moreover note \<open>cofinal(A,\<gamma>,_)\<close>
+  ultimately
+  have "cf_fun(f,\<gamma>)"
+    using cofinal_range_iff_cofinal_fun by blast
+  moreover from \<open>Ord(\<alpha>)\<close>
+  obtain h where "h :cf(\<alpha>) \<rightarrow>\<^sub>< \<alpha>" "cf_fun(h,\<alpha>)"
+    using cofinal_mono_map_cf by blast
+  moreover from \<open>Ord(\<gamma>)\<close>
+  have "trans(Memrel(\<gamma>))"
+    using trans_Memrel by simp
+  moreover
+  note \<open>A\<subseteq>\<gamma>\<close>
+  ultimately
+  have "cofinal_fun(f O h,\<gamma>,Memrel(\<gamma>))"
+    using cofinal_comp ord_iso_is_mono_map[OF \<open>f:\<langle>\<alpha>,_\<rangle> \<cong> \<langle>A,_\<rangle>\<close>] mono_map_is_fun
+      mono_map_mono by blast
+  moreover from \<open>f:\<alpha>\<rightarrow>A\<close> \<open>A\<subseteq>\<gamma>\<close> \<open>h\<in>mono_map(cf(\<alpha>),_,\<alpha>,_)\<close>
+  have "f O h : cf(\<alpha>) \<rightarrow> \<gamma>"
+    using Pi_mono[of A \<gamma>] comp_fun  mono_map_is_fun by blast
+  moreover
+  note \<open>Ord(\<gamma>)\<close> \<open>Ord(\<alpha>)\<close> \<open>\<alpha> = ordertype(A,Memrel(\<gamma>))\<close>
+  ultimately
+  show "cf(\<gamma>) \<le> cf(ordertype(A,Memrel(\<gamma>)))"
+    using cf_le_domain_cofinal_fun[of _ _ "f O h"]
+    by (auto simp add:cf_fun_def)
+      (********************************************************)
+  from \<open>f:\<langle>\<alpha>, _\<rangle> \<cong> \<langle>A,_\<rangle>\<close> \<open>A\<subseteq>\<gamma>\<close>
+  have "f :\<alpha> \<rightarrow>\<^sub>< \<gamma>"
+    using mono_map_mono[OF ord_iso_is_mono_map] by simp
+  then
+  have "f: \<alpha> \<rightarrow> \<gamma>"
+    using mono_map_is_fun by simp
+  with \<open>cf_fun(f,\<gamma>)\<close> \<open>Limit(\<gamma>)\<close> \<open>Ord(\<alpha>)\<close>
+  obtain g where "g :cf(\<gamma>) \<rightarrow>\<^sub>< \<alpha>"
+    "f O g :cf(\<gamma>) \<rightarrow>\<^sub>< \<gamma>"
+    "cofinal_fun(f O g,\<gamma>,Memrel(\<gamma>))"
+    using cofinal_fun_factorization by blast
+  moreover from this
+  have "g:cf(\<gamma>)\<rightarrow>\<alpha>"
+    using mono_map_is_fun by simp
+  moreover
+  note \<open>Ord(\<alpha>)\<close>
+  moreover from calculation and \<open>f :\<alpha> \<rightarrow>\<^sub>< \<gamma>\<close> \<open>Ord(\<gamma>)\<close>
+  have "cf_fun(g,\<alpha>)"
+    using factor_is_cofinal by blast
+  moreover
+  note \<open>\<alpha> = ordertype(A,Memrel(\<gamma>))\<close>
+  ultimately
+  show "cf(ordertype(A,Memrel(\<gamma>))) \<le> cf(\<gamma>)"
+    using cf_le_domain_cofinal_fun[OF _ Ord_cf mono_map_is_fun] by simp
+qed
+
+lemma cf_idemp:
+  assumes "Limit(\<gamma>)"
+  shows "cf(\<gamma>) = cf(cf(\<gamma>))"
+proof -
+  from assms
+  obtain A where "A\<subseteq>\<gamma>" "cofinal(A,\<gamma>,Memrel(\<gamma>))" "cf(\<gamma>) = ordertype(A,Memrel(\<gamma>))"
+    using Limit_is_Ord cf_is_ordertype by blast
+  with assms
+  have "cf(\<gamma>) = cf(ordertype(A,Memrel(\<gamma>)))" using cf_ordertype_cofinal by simp
+  also
+  have "... = cf(cf(\<gamma>))"
+    using \<open>cf(\<gamma>) = ordertype(A,Memrel(\<gamma>))\<close> by simp
+  finally
+  show "cf(\<gamma>) = cf(cf(\<gamma>))"  .
+qed
+
+lemma cf_le_cardinal:
+  assumes "Limit(\<gamma>)"
+  shows "cf(\<gamma>) \<le> |\<gamma>|"
+proof -
+  from assms
+  have \<open>Ord(\<gamma>)\<close> using Limit_is_Ord by simp
+  then
+  obtain f where "f \<in> surj(|\<gamma>|,\<gamma>)"
+    using Ord_cardinal_eqpoll unfolding eqpoll_def bij_def by blast
+  with \<open>Ord(\<gamma>)\<close>
+  show ?thesis
+    using Card_is_Ord[OF Card_cardinal] surj_is_cofinal
+      cf_le_domain_cofinal_fun[of \<gamma>] surj_is_fun by blast
+qed
+
+lemma regular_is_Card:
+  notes le_imp_subset [dest]
+  assumes "Limit(\<gamma>)" "\<gamma> = cf(\<gamma>)"
+  shows "Card(\<gamma>)"
+proof -
+  from assms
+  have "|\<gamma>| \<subseteq> \<gamma>"
+    using Limit_is_Ord Ord_cardinal_le by blast
+  also from \<open>\<gamma> = cf(\<gamma>)\<close>
+  have "\<gamma> \<subseteq> cf(\<gamma>)" by simp
+  finally
+  have "|\<gamma>| \<subseteq> cf(\<gamma>)" .
+  with assms
+  show ?thesis unfolding Card_def using cf_le_cardinal by force
+qed
+
+lemma Limit_cf: assumes "Limit(\<kappa>)" shows "Limit(cf(\<kappa>))"
+  using Ord_cf[of \<kappa>, THEN Ord_cases]
+    \<comment> \<open>\<^term>\<open>cf(\<kappa>)\<close> being 0 or successor leads to contradiction\<close>
+proof (cases)
+  case 1
+  with \<open>Limit(\<kappa>)\<close>
+  show ?thesis using cf_zero_iff Limit_is_Ord by simp
+next
+  case (2 \<alpha>)
+  moreover
+  note \<open>Limit(\<kappa>)\<close>
+  moreover from calculation
+  have "cf(\<kappa>) = 1"
+    using cf_idemp cf_succ by fastforce
+  ultimately
+  show ?thesis
+    using succ_LimitE cf_eq_one_iff Limit_is_Ord
+    by auto
+qed
+
+lemma InfCard_cf: "Limit(\<kappa>) \<Longrightarrow> InfCard(cf(\<kappa>))"
+  using regular_is_Card cf_idemp Limit_cf nat_le_Limit Limit_cf
+  unfolding InfCard_def by simp
+
+lemma cf_le_cf_fun:
+  notes [dest] = Limit_is_Ord
+  assumes "cf(\<kappa>) \<le> \<nu>" "Limit(\<kappa>)"
+  shows "\<exists>f.  f:\<nu> \<rightarrow> \<kappa>  \<and>  cf_fun(f, \<kappa>)"
+proof -
+  note assms
+  moreover from this
+  obtain h where h_cofinal_mono: "cf_fun(h,\<kappa>)"
+    "h :cf(\<kappa>) \<rightarrow>\<^sub>< \<kappa>"
+    "h : cf(\<kappa>) \<rightarrow> \<kappa>"
+    using cofinal_mono_map_cf mono_map_is_fun by force
+  moreover from calculation
+  obtain g where "g \<in> inj(cf(\<kappa>), \<nu>)"
+    using le_imp_lepoll by blast
+  from this and calculation(2,3,5)
+  obtain f where "f \<in> surj(\<nu>, cf(\<kappa>))" "f: \<nu> \<rightarrow> cf(\<kappa>)"
+    using inj_imp_surj[OF _ Limit_has_0[THEN ltD]]
+      surj_is_fun Limit_cf by blast
+  moreover from this
+  have "cf_fun(f,cf(\<kappa>))"
+    using surj_is_cofinal by simp
+  moreover
+  note h_cofinal_mono \<open>Limit(\<kappa>)\<close>
+  moreover from calculation
+  have "cf_fun(h O f,\<kappa>)"
+    using cf_fun_comp by blast
+  moreover from calculation
+  have "h O f \<in> \<nu> -> \<kappa>"
+    using comp_fun by simp
+  ultimately
+  show ?thesis by blast
+qed
+
+lemma Limit_cofinal_fun_lt:
+  notes [dest] = Limit_is_Ord
+  assumes "Limit(\<kappa>)" "f: \<nu> \<rightarrow> \<kappa>" "cf_fun(f,\<kappa>)" "n\<in>\<kappa>"
+  shows "\<exists>\<alpha>\<in>\<nu>. n < f`\<alpha>"
+proof -
+  from \<open>Limit(\<kappa>)\<close> \<open>n\<in>\<kappa>\<close>
+  have "succ(n) \<in> \<kappa>"
+    using Limit_has_succ[OF _ ltI, THEN ltD] by auto
+  moreover
+  note \<open>f: \<nu> \<rightarrow> _\<close>
+  moreover from this
+  have "domain(f) = \<nu>"
+    using domain_of_fun by simp
+  moreover
+  note \<open>cf_fun(f,\<kappa>)\<close>
+  ultimately
+  obtain \<alpha> where "\<alpha> \<in> \<nu>" "succ(n) \<in> f`\<alpha> \<or> succ(n) = f `\<alpha>"
+    using cf_funD[THEN cofinal_funD] by blast
+  moreover from this
+  consider (1) "succ(n) \<in> f`\<alpha>" | (2) "succ(n) = f `\<alpha>"
+    by blast
+  then
+  have "n < f`\<alpha>"
+  proof (cases)
+    case 1
+    moreover
+    have "n \<in> succ(n)" by simp
+    moreover
+    note \<open>Limit(\<kappa>)\<close> \<open>f: \<nu> \<rightarrow> _\<close> \<open>\<alpha> \<in> \<nu>\<close>
+    moreover from this
+    have "Ord(f ` \<alpha>)"
+      using apply_type[of f \<nu> "\<lambda>_. \<kappa>", THEN [2] Ord_in_Ord]
+      by blast
+    ultimately
+    show ?thesis
+      using Ord_trans[of n "succ(n)" "f ` \<alpha>"] ltI  by blast
+  next
+    case 2
+    have "n \<in> f ` \<alpha>" by (simp add:2[symmetric])
+    with \<open>Limit(\<kappa>)\<close> \<open>f: \<nu> \<rightarrow> _\<close> \<open>\<alpha> \<in> \<nu>\<close>
+    show ?thesis
+      using ltI
+        apply_type[of f \<nu> "\<lambda>_. \<kappa>", THEN [2] Ord_in_Ord]
+      by blast
+  qed
+  ultimately
+  show ?thesis by blast
+qed
+
+context
+  includes Ord_dests Aleph_dests Aleph_intros Aleph_mem_dests mono_map_rules
+begin
+
+text\<open>We end this section by calculating the cofinality of Alephs, for
+the zero and limit case. The successor case depends on $\AC$.\<close>
+
+lemma cf_nat: "cf(\<omega>) = \<omega>"
+  using Limit_nat[THEN InfCard_cf] cf_le_cardinal[of \<omega>]
+    Card_nat[THEN Card_cardinal_eq] le_anti_sym
+  unfolding InfCard_def by auto
+
+lemma cf_Aleph_zero: "cf(\<aleph>\<^bsub>0\<^esub>) = \<aleph>\<^bsub>0\<^esub>" 
+  using cf_nat unfolding Aleph_def by simp
+
+lemma cf_Aleph_Limit:
+  assumes "Limit(\<gamma>)"
+  shows "cf(\<aleph>\<^bsub>\<gamma>\<^esub>) = cf(\<gamma>)" 
+proof -
+  note \<open>Limit(\<gamma>)\<close>
+  moreover from this
+  have "(\<lambda>x\<in>\<gamma>. \<aleph>\<^bsub>x\<^esub>) : \<gamma> \<rightarrow> \<aleph>\<^bsub>\<gamma>\<^esub>" (is "?f : _ \<rightarrow> _")
+    using lam_funtype[of _ Aleph] fun_weaken_type[of _ _ _ "\<aleph>\<^bsub>\<gamma>\<^esub>"] by blast
+  moreover from \<open>Limit(\<gamma>)\<close>
+  have "x \<in> y \<Longrightarrow> \<aleph>\<^bsub>x\<^esub> \<in> \<aleph>\<^bsub>y\<^esub>" if "x \<in> \<gamma>" "y \<in> \<gamma>" for x y
+    using that Ord_in_Ord[of \<gamma>] Ord_trans[of _ _ \<gamma>] by blast
+  ultimately
+  have "?f \<in> mono_map(\<gamma>,Memrel(\<gamma>),\<aleph>\<^bsub>\<gamma>\<^esub>, Memrel(\<aleph>\<^bsub>\<gamma>\<^esub>))"
+    by auto
+  with  \<open>Limit(\<gamma>)\<close> 
+  have "?f \<in> \<langle>\<gamma>, Memrel(\<gamma>)\<rangle> \<cong> \<langle>?f``\<gamma>, Memrel(\<aleph>\<^bsub>\<gamma>\<^esub>)\<rangle>"
+    using mono_map_imp_ord_iso_Memrel[of \<gamma> "\<aleph>\<^bsub>\<gamma>\<^esub>" ?f] 
+      Card_Aleph (* Already an intro rule, but need it explicitly *)
+    by blast
+  then
+  have "converse(?f) \<in> \<langle>?f``\<gamma>, Memrel(\<aleph>\<^bsub>\<gamma>\<^esub>)\<rangle> \<cong> \<langle>\<gamma>, Memrel(\<gamma>)\<rangle>"
+    using ord_iso_sym by simp
+  with \<open>Limit(\<gamma>)\<close>
+  have "ordertype(?f``\<gamma>, Memrel(\<aleph>\<^bsub>\<gamma>\<^esub>)) = \<gamma>"
+    using ordertype_eq[OF _ well_ord_Memrel]
+    ordertype_Memrel by auto
+  moreover from \<open>Limit(\<gamma>)\<close>
+  have "cofinal(?f``\<gamma>, \<aleph>\<^bsub>\<gamma>\<^esub>, Memrel(\<aleph>\<^bsub>\<gamma>\<^esub>))" 
+    unfolding cofinal_def 
+  proof (standard, intro ballI)
+    fix a
+    assume "a\<in>\<aleph>\<^bsub>\<gamma>\<^esub>" "\<aleph>\<^bsub>\<gamma>\<^esub> = (\<Union>i<\<gamma>. \<aleph>\<^bsub>i\<^esub>)"
+    moreover from this
+    obtain i where "i<\<gamma>" "a\<in>\<aleph>\<^bsub>i\<^esub>"
+      by auto
+    moreover from this and \<open>Limit(\<gamma>)\<close>
+    have "Ord(i)" using ltD Ord_in_Ord by blast
+    moreover from \<open>Limit(\<gamma>)\<close> and calculation
+    have "succ(i) \<in> \<gamma>" using ltD by auto
+    moreover from this and \<open>Ord(i)\<close>
+    have "\<aleph>\<^bsub>i\<^esub> < \<aleph>\<^bsub>succ(i)\<^esub>" 
+      by (auto) 
+    ultimately
+    have "\<langle>a,\<aleph>\<^bsub>i\<^esub>\<rangle> \<in> Memrel(\<aleph>\<^bsub>\<gamma>\<^esub>)"
+      using ltD by (auto dest:Aleph_increasing)
+    moreover from \<open>i<\<gamma>\<close>
+    have "\<aleph>\<^bsub>i\<^esub> \<in> ?f``\<gamma>" 
+      using ltD apply_in_image[OF \<open>?f : _ \<rightarrow> _\<close>] by auto
+    ultimately
+    show "\<exists>x\<in>?f `` \<gamma>. \<langle>a, x\<rangle> \<in> Memrel(\<aleph>\<^bsub>\<gamma>\<^esub>) \<or> a = x" by blast
+  qed
+  moreover
+  note \<open>?f: \<gamma> \<rightarrow> \<aleph>\<^bsub>\<gamma>\<^esub>\<close> \<open>Limit(\<gamma>)\<close>
+  ultimately
+  show "cf(\<aleph>\<^bsub>\<gamma>\<^esub>) =  cf(\<gamma>)"
+    using cf_ordertype_cofinal[OF Limit_Aleph Image_sub_codomain, of \<gamma> ?f \<gamma> \<gamma> ] 
+      Limit_is_Ord by simp 
+qed
+
+end (* includes *)
+
+end
\ No newline at end of file
diff --git a/thys/Delta_System_Lemma/Cohen_Posets.thy b/thys/Delta_System_Lemma/Cohen_Posets.thy
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/Cohen_Posets.thy
@@ -0,0 +1,248 @@
+subsection\<open>Application to Cohen posets\label{sec:cohen}\<close>
+
+theory Cohen_Posets
+  imports 
+    Delta_System
+
+begin
+
+text\<open>We end this session by applying DSL to the combinatorics of
+finite function posets. We first define some basic concepts; we take
+a different approach from \cite{2020arXiv200109715G}, in that the
+order relation is presented as a predicate (of type @{typ \<open>[i,i] \<Rightarrow> o\<close>}). 
+
+Two elements of a poset are \<^emph>\<open>compatible\<close> if they have a common lower
+bound.\<close>
+
+definition compat_in :: "[i,[i,i]\<Rightarrow>o,i,i]\<Rightarrow>o" where
+  "compat_in(A,r,p,q) \<equiv> \<exists>d\<in>A . r(d,p) \<and> r(d,q)"
+
+text\<open>An \<^emph>\<open>antichain\<close> is a subset of pairwise incompatible members.\<close>
+
+definition
+  antichain :: "[i,[i,i]\<Rightarrow>o,i]\<Rightarrow>o" where
+  "antichain(P,leq,A) \<equiv> A\<subseteq>P \<and> (\<forall>p\<in>A. \<forall>q\<in>A.
+                p\<noteq>q \<longrightarrow> \<not>compat_in(P,leq,p,q))"
+
+text\<open>A poset has the  \<^emph>\<open>countable chain condition\<close> (ccc) if all of its
+antichains are countable.\<close>
+
+definition
+  ccc :: "[i,[i,i]\<Rightarrow>o]\<Rightarrow>o" where
+  "ccc(P,leq) \<equiv> \<forall>A. antichain(P,leq,A) \<longrightarrow> countable(A)"
+
+text\<open>Finally, the \<^emph>\<open>Cohen poset\<close> is the set of finite partial functions
+between two sets with the order of reverse inclusion.\<close>
+
+definition
+  Fn :: "[i,i] \<Rightarrow> i" where
+  "Fn(I,J) \<equiv> \<Union>{(d\<rightarrow>J) . d \<in> {x \<in> Pow(I).  Finite(x)}}"
+
+abbreviation
+  Supset :: "i \<Rightarrow> i \<Rightarrow> o" (infixl \<open>\<supseteq>\<close> 50) where
+  "f \<supseteq> g \<equiv> g \<subseteq> f"
+
+lemma FnI[intro]:
+  assumes "p : d \<rightarrow> J" "d \<subseteq> I" "Finite(d)"
+  shows "p \<in> Fn(I,J)"
+  using assms unfolding Fn_def by auto
+
+lemma FnD[dest]:
+  assumes "p \<in> Fn(I,J)"
+  shows "\<exists>d. p : d \<rightarrow> J \<and> d \<subseteq> I \<and> Finite(d)"
+  using assms unfolding Fn_def by auto
+
+lemma Fn_is_function: "p \<in> Fn(I,J) \<Longrightarrow> function(p)"
+  unfolding Fn_def using fun_is_function by auto
+
+lemma restrict_eq_imp_compat:
+  assumes "f \<in> Fn(I, J)" "g \<in> Fn(I, J)"
+    "restrict(f, domain(f) \<inter> domain(g)) = restrict(g, domain(f) \<inter> domain(g))"
+  shows "f \<union> g \<in> Fn(I, J)"
+proof -
+  from assms
+  obtain d1 d2 where "f : d1 \<rightarrow> J" "d1 \<in> Pow(I)" "Finite(d1)"
+    "g : d2 \<rightarrow> J" "d2 \<in> Pow(I)" "Finite(d2)"
+    by blast
+  with assms
+  show ?thesis
+    using domain_of_fun
+      restrict_eq_imp_Un_into_Pi[of f d1 "\<lambda>_. J" g d2 "\<lambda>_. J"]
+    by auto
+qed
+
+text\<open>We finally arrive to our application of DSL.\<close>
+
+lemma ccc_Fn_nat: "ccc(Fn(I,2), (\<supseteq>))"
+proof -
+  {
+    fix A
+    assume "\<not> countable(A)"
+    assume "A \<subseteq> Fn(I, 2)"
+    moreover from this
+    have "countable({p\<in>A. domain(p) = d})" for d
+    proof (cases "Finite(d) \<and> d \<subseteq> I")
+      case True
+      with \<open>A \<subseteq> Fn(I, 2)\<close>
+      have "{p \<in> A . domain(p) = d} \<subseteq> d \<rightarrow> 2"
+        using domain_of_fun by fastforce
+      moreover from True
+      have "Finite(d \<rightarrow> 2)"
+        using Finite_Pi lesspoll_nat_is_Finite by auto
+      ultimately
+      show ?thesis using subset_Finite[of _ "d\<rightarrow>2" ] Finite_imp_countable
+        by auto
+    next
+      case False
+      with \<open>A \<subseteq> Fn(I, 2)\<close>
+      have "{p \<in> A . domain(p) = d} = 0"
+        by (intro equalityI) (auto dest!: domain_of_fun)
+      then
+      show ?thesis using empty_lepollI by auto
+    qed
+    moreover
+    have "uncountable({domain(p) . p \<in> A})"
+    proof
+      from \<open>A \<subseteq> Fn(I, 2)\<close>
+      have "A = (\<Union>d\<in>{domain(p) . p \<in> A}. {p\<in>A. domain(p) = d})"
+        by auto
+      moreover
+      assume "countable({domain(p) . p \<in> A})"
+      moreover
+      note \<open>\<And>d. countable({p\<in>A. domain(p) = d})\<close> \<open>\<not>countable(A)\<close>
+      ultimately
+      show "False"
+        using countable_imp_countable_UN[of "{domain(p). p\<in>A}"
+            "\<lambda>d. {p \<in> A. domain(p) = d }"]
+        by auto
+    qed
+    moreover from \<open>A \<subseteq> Fn(I, 2)\<close>
+    have "p \<in> A \<Longrightarrow> Finite(domain(p))" for p
+      using lesspoll_nat_is_Finite[of "domain(p)"]
+        domain_of_fun[of p _ "\<lambda>_. 2"] by auto
+    ultimately
+    obtain D where "delta_system(D)" "D \<subseteq> {domain(p) . p \<in> A}" "D \<approx> \<aleph>\<^bsub>1\<^esub>"
+      using delta_system_uncountable[of "{domain(p) . p \<in> A}"] by auto
+    then
+    have delta:"\<forall>d1\<in>D. \<forall>d2\<in>D. d1 \<noteq> d2 \<longrightarrow> d1 \<inter> d2 = \<Inter>D"
+      using delta_system_root_eq_Inter
+      by simp
+    moreover from \<open>D \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
+    have "uncountable(D)"
+      using uncountable_iff_subset_eqpoll_Aleph1 by auto
+    moreover from this and \<open>D \<subseteq> {domain(p) . p \<in> A}\<close>
+    obtain p1 where "p1 \<in> A" "domain(p1) \<in> D"
+      using uncountable_not_empty[of D] by blast
+    moreover from this and \<open>p1 \<in> A \<Longrightarrow> Finite(domain(p1))\<close>
+    have "Finite(domain(p1))" using Finite_domain by simp
+    moreover
+    define r where "r \<equiv> \<Inter>D"
+    ultimately
+    have "Finite(r)" using subset_Finite[of "r" "domain(p1)"] by auto
+    have "countable({restrict(p,r) . p\<in>A})"
+    proof -
+      have "f \<in> Fn(I, 2) \<Longrightarrow> restrict(f,r) \<in> Pow(r \<times> 2)" for f
+        using restrict_subset_Sigma[of f _ "\<lambda>_. 2" r]
+        by (auto dest!:FnD simp: Pi_def) auto
+      with \<open>A \<subseteq> Fn(I, 2)\<close>
+      have "{restrict(f,r) . f \<in> A } \<subseteq> Pow(r \<times> 2)"
+        by fast
+      with \<open>Finite(r)\<close>
+      show ?thesis
+        using Finite_Sigma[THEN Finite_Pow, of r "\<lambda>_. 2"]
+        by (intro Finite_imp_countable) (auto intro:subset_Finite)
+    qed
+    moreover
+    have "uncountable({p\<in>A. domain(p) \<in> D})" (is "uncountable(?X)")
+    proof
+      from \<open>D \<subseteq> {domain(p) . p \<in> A}\<close>
+      have "(\<lambda>p\<in>?X. domain(p)) \<in> surj(?X, D)"
+        using lam_type unfolding surj_def by auto
+      moreover
+      assume "countable(?X)"
+      moreover
+      note \<open>uncountable(D)\<close>
+      ultimately
+      show False
+        using surj_countable by auto
+    qed
+    moreover
+    have "D = (\<Union>f\<in>Pow(r\<times>2) . {domain(p) . p\<in>{ x\<in>A. restrict(x,r) = f \<and> domain(x) \<in> D}})"
+    proof -
+      {
+        fix z
+        assume "z \<in> D"
+        with \<open>D \<subseteq> _\<close>
+        obtain p  where "domain(p) = z" "p \<in> A"
+          by auto
+        moreover from \<open>A \<subseteq> Fn(I, 2)\<close> and this
+        have "p : z \<rightarrow> 2"
+          using domain_of_fun by (auto dest!:FnD)
+        moreover from this
+        have "restrict(p,r) \<subseteq> r \<times> 2"
+          using function_restrictI[of p r] fun_is_function[of p z "\<lambda>_. 2"]
+            restrict_subset_Sigma[of p z "\<lambda>_. 2" r]
+          by (auto simp:Pi_def)
+        ultimately
+        have "\<exists>p\<in>A.  restrict(p,r) \<in> Pow(r\<times>2) \<and> domain(p) = z" by auto
+      }
+      then
+      show ?thesis
+        by (intro equalityI) (force)+
+    qed
+    obtain f where "uncountable({domain(p) . p\<in>{x\<in>A. restrict(x,r) = f \<and> domain(x) \<in> D}})"
+      (is "uncountable(?Y(f))")
+    proof -
+      {
+        from \<open>Finite(r)\<close>
+        have "countable(Pow(r\<times>2))"
+          using Finite_Sigma[THEN Finite_Pow, THEN Finite_imp_countable]
+          by simp
+        moreover
+        assume "countable(?Y(f))" for f
+        moreover
+        note \<open>D = (\<Union>f\<in>Pow(r\<times>2) .?Y(f))\<close>
+        moreover
+        note \<open>uncountable(D)\<close>
+        ultimately
+        have "False"
+          using countable_imp_countable_UN[of "Pow(r\<times>2)" ?Y] by auto
+      }
+      with that
+      show ?thesis by auto
+    qed
+    then
+    obtain j where "j \<in> inj(nat, ?Y(f))"
+      using uncountable_iff_nat_lt_cardinal[THEN iffD1, THEN leI,
+          THEN cardinal_le_imp_lepoll, THEN lepollD]
+      by auto
+    then
+    have "j`0 \<noteq> j`1" "j`0 \<in> ?Y(f)" "j`1 \<in> ?Y(f)"
+      using inj_is_fun[THEN apply_type, of j nat "?Y(f)"]
+      unfolding inj_def by auto
+    then
+    obtain p q where "domain(p) \<noteq> domain(q)" "p \<in> A" "q \<in> A"
+      "domain(p) \<in> D" "domain(q) \<in> D"
+      "restrict(p,r) = restrict(q,r)" by auto
+    moreover from this and delta
+    have "domain(p) \<inter> domain(q) = r" unfolding r_def by simp
+    moreover
+    note \<open>A \<subseteq> Fn(I, 2)\<close>
+    moreover from calculation
+    have "p \<union> q \<in> Fn(I, 2)"
+      by (rule_tac restrict_eq_imp_compat) auto
+    ultimately
+    have "\<exists>p\<in>A. \<exists>q\<in>A. p \<noteq> q \<and> compat_in(Fn(I, 2), (\<supseteq>), p, q)"
+      unfolding compat_in_def
+      by (rule_tac bexI[of _ p], rule_tac bexI[of _ q]) blast
+  }
+  then
+  show ?thesis unfolding ccc_def antichain_def by auto
+qed
+
+text\<open>The fact that a poset $P$ has the ccc has useful consequences for the
+theory of forcing, since it implies that cardinals from the original
+model are exactly the cardinals in any generic extension by $P$
+\cite[Chap.~IV]{kunen2011set}.\<close>
+
+end
\ No newline at end of file
diff --git a/thys/Delta_System_Lemma/Delta_System.thy b/thys/Delta_System_Lemma/Delta_System.thy
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/Delta_System.thy
@@ -0,0 +1,274 @@
+section\<open>The Delta System Lemma\label{sec:dsl}\<close>
+
+theory Delta_System
+  imports 
+    Cardinal_Library
+
+begin
+
+text\<open>A \<^emph>\<open>delta system\<close> is family of sets with a common pairwise
+intersection.\<close>
+
+definition
+  delta_system :: "i \<Rightarrow> o" where
+  "delta_system(D) \<equiv> \<exists>r. \<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
+
+lemma delta_systemI[intro]: 
+  assumes "\<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
+  shows "delta_system(D)"
+  using assms unfolding delta_system_def by simp
+
+lemma delta_systemD[dest]:
+  "delta_system(D) \<Longrightarrow> \<exists>r. \<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
+  unfolding delta_system_def by simp
+
+text\<open>Hence, pairwise intersections equal the intersection of the whole
+family.\<close>
+
+lemma delta_system_root_eq_Inter:
+  assumes "delta_system(D)"
+  shows "\<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = \<Inter>D"
+proof (clarify, intro equalityI, auto)
+  fix A' B' x C
+  assume hyp:"A'\<in>D" "B'\<in> D" "A'\<noteq>B'" "x\<in>A'" "x\<in>B'" "C\<in>D"
+  with assms
+  obtain r where delta:"\<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
+    by auto
+  show "x \<in> C"
+  proof (cases "C=A'")
+    case True
+    with hyp and assms
+    show ?thesis by simp
+  next
+    case False
+    moreover
+    note hyp
+    moreover from calculation and delta
+    have "r = C \<inter> A'" "A' \<inter> B' = r" "x\<in>r" by auto
+    ultimately
+    show ?thesis by simp
+  qed
+qed
+
+text\<open>The \<^emph>\<open>Delta System Lemma\<close> (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>\<open>\<aleph>\<^bsub>1\<^esub>\<close>  assume
+some weak versions of the generalized continuum hypothesis for the
+cardinals involved.
+
+The proof is essentially the one in \cite[III.2.6]{kunen2011set} for the
+case  \<^term>\<open>\<aleph>\<^bsub>1\<^esub>\<close>; another similar presentation can be found in
+\cite[Chap.~16]{JW}.\<close>
+
+lemma delta_system_Aleph1:
+  assumes "\<forall>A\<in>F. Finite(A)" "F \<approx> \<aleph>\<^bsub>1\<^esub>"
+  shows "\<exists>D. D \<subseteq> F \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
+proof -
+  text\<open>Since all members are finite,\<close>
+  from \<open>\<forall>A\<in>F. Finite(A)\<close>
+  have "(\<lambda>A\<in>F. |A|) : F \<rightarrow> \<omega>" (is "?cards : _")
+    by (rule_tac lam_type) simp
+  moreover from this
+  have a:"?cards -`` {n} = { A\<in>F . |A| = n }" for n
+    using vimage_lam by auto
+  moreover
+  note \<open>F \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
+  moreover from calculation
+  text\<open>there are uncountably many have the same cardinal:\<close>
+  obtain n where "n\<in>\<omega>" "|?cards -`` {n}| = \<aleph>\<^bsub>1\<^esub>"
+    using eqpoll_Aleph1_cardinal_vimage[of F ?cards] by auto
+  moreover
+  define G where "G \<equiv> ?cards -`` {n}"
+  moreover from calculation
+  have "G \<subseteq> F" by auto
+  ultimately
+  text\<open>Therefore, without loss of generality, we can assume that all
+  elements of the family have cardinality \<^term>\<open>n\<in>\<omega>\<close>.\<close>
+  have "A\<in>G \<Longrightarrow> |A| = n" and "G \<approx> \<aleph>\<^bsub>1\<^esub>" for A
+    using cardinal_Card_eqpoll_iff by auto
+  with \<open>n\<in>\<omega>\<close>
+  text\<open>So we prove the result by induction on this \<^term>\<open>n\<close> and
+  generalizing \<^term>\<open>G\<close>, since the argument requires changing the
+  family in order to apply the inductive hypothesis.\<close>
+  have "\<exists>D. D \<subseteq> G \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
+  proof (induct arbitrary:G)
+    case 0 \<comment> \<open>This case is impossible\<close>
+    then
+    have "G \<subseteq> {0}"
+      using cardinal_0_iff_0 by auto
+    with \<open>G \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
+    show ?case
+      using nat_lt_Aleph1 subset_imp_le_cardinal[of G "{0}"]
+        lt_trans2 cardinal_Card_eqpoll_iff by auto
+  next
+    case (succ n)
+    then
+    have "\<forall>a\<in>G. Finite(a)"
+      using Finite_cardinal_iff' nat_into_Finite[of "succ(n)"]
+      by fastforce
+    show "\<exists>D. D \<subseteq> G \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
+    proof (cases "\<exists>p. {A\<in>G . p \<in> A} \<approx> \<aleph>\<^bsub>1\<^esub>")
+      case True \<comment> \<open>the positive case, uncountably many sets with a
+                    common element\<close>
+      then
+      obtain p where "{A\<in>G . p \<in> A} \<approx> \<aleph>\<^bsub>1\<^esub>" by blast
+      moreover from this
+      have "{A-{p} . A\<in>{X\<in>G. p\<in>X}} \<approx> \<aleph>\<^bsub>1\<^esub>" (is "?F \<approx> _")
+        using Diff_bij[of "{A\<in>G . p \<in> A}" "{p}"]
+          comp_bij[OF bij_converse_bij, where C="\<aleph>\<^bsub>1\<^esub>"] by fast
+      text\<open>Now using the hypothesis of the successor case,\<close>
+      moreover from \<open>\<And>A. A\<in>G \<Longrightarrow> |A|=succ(n)\<close> \<open>\<forall>a\<in>G. Finite(a)\<close>
+        and this
+      have "p\<in>A \<Longrightarrow> A\<in>G \<Longrightarrow> |A - {p}| = n" for A
+        using Finite_imp_succ_cardinal_Diff[of _ p] by force
+      moreover from this and \<open>n\<in>\<omega>\<close>
+      have "\<forall>a\<in>?F. Finite(a)"
+        using Finite_cardinal_iff' nat_into_Finite by auto
+      moreover
+      text\<open>we may apply the inductive hypothesis to the new family \<^term>\<open>?F\<close>:\<close>
+      note \<open>(\<And>A. A \<in> ?F \<Longrightarrow> |A| = n) \<Longrightarrow> ?F \<approx> \<aleph>\<^bsub>1\<^esub> \<Longrightarrow>
+             \<exists>D. D \<subseteq> ?F \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
+      ultimately
+      obtain D where "D\<subseteq>{A-{p} . A\<in>{X\<in>G. p\<in>X}}" "delta_system(D)" "D \<approx> \<aleph>\<^bsub>1\<^esub>"
+        by auto
+      moreover from this
+      obtain r where "\<forall>A\<in>D. \<forall>B\<in>D. A \<noteq> B \<longrightarrow> A \<inter> B = r"
+        by fastforce
+      then
+      have "\<forall>A\<in>D.\<forall>B\<in>D. A\<union>{p} \<noteq> B\<union>{p}\<longrightarrow>(A \<union> {p}) \<inter> (B \<union> {p}) = r\<union>{p}"
+        by blast
+      ultimately
+      have "delta_system({B \<union> {p} . B\<in>D})" (is "delta_system(?D)")
+        by fastforce
+      moreover from \<open>D \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
+      have "|D| = \<aleph>\<^bsub>1\<^esub>" "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 \<approx> \<aleph>\<^bsub>1\<^esub>"
+        using cardinal_map_Un[of D "{p}"] naturals_lt_nat
+          cardinal_eqpoll_iff[THEN iffD1] by simp
+      moreover
+      note \<open>D \<subseteq> {A-{p} . A\<in>{X\<in>G. p\<in>X}}\<close>
+      have "?D \<subseteq> G"
+      proof -
+        {
+          fix A
+          assume "A\<in>G" "p\<in>A"
+          moreover from this
+          have "A = A - {p} \<union> {p}"
+            by blast
+          ultimately
+          have "A -{p} \<union> {p} \<in> G"
+            by auto
+        }
+        with \<open>D \<subseteq> {A-{p} . A\<in>{X\<in>G. p\<in>X}}\<close>
+        show ?thesis
+          by blast
+      qed
+      ultimately
+      show "\<exists>D. D \<subseteq> G \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>" by auto
+    next
+      case False
+      note \<open>\<not> (\<exists>p. {A \<in> G . p \<in> A} \<approx> \<aleph>\<^bsub>1\<^esub>)\<close> \<comment> \<open>the other case\<close>
+      moreover from \<open>G \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
+      have "{A \<in> G . p \<in> A} \<lesssim> \<aleph>\<^bsub>1\<^esub>" (is "?G(p) \<lesssim> _") for p
+        by (blast intro:lepoll_eq_trans[OF subset_imp_lepoll])
+      ultimately
+      have "?G(p) \<prec> \<aleph>\<^bsub>1\<^esub>" for p
+        unfolding lesspoll_def by simp
+      then (* may omit the previous step if unfolding here: *)
+      have "?G(p) \<lesssim> \<omega>" for p
+        using lesspoll_aleph_plus_one[of 0] Aleph_zero_eq_nat by auto
+      moreover
+      have "{A \<in> G . S \<inter> A \<noteq> 0} = (\<Union>p\<in>S. ?G(p))" for S
+        by auto
+      ultimately
+      have "countable(S) \<Longrightarrow> countable({A \<in> G . S \<inter> A \<noteq> 0})" for S
+        using InfCard_nat Card_nat
+         le_Card_iff[THEN iffD2, THEN [3] leqpoll_imp_cardinal_UN_le,
+           THEN [2] le_Card_iff[THEN iffD1], of \<omega> S]
+        unfolding countable_def by simp
+      text\<open>For every countable subfamily of \<^term>\<open>G\<close> there is another some
+      element disjoint from all of them:\<close>
+      have "\<exists>A\<in>G. \<forall>S\<in>X. S \<inter> A = 0" if "|X| < \<aleph>\<^bsub>1\<^esub>" "X \<subseteq> G" for X
+      proof -
+        from \<open>n\<in>\<omega>\<close> \<open>\<And>A. A\<in>G \<Longrightarrow> |A| = succ(n)\<close>
+        have "A\<in>G \<Longrightarrow> Finite(A)" for A
+          using cardinal_Card_eqpoll_iff
+          unfolding Finite_def by fastforce
+        with \<open>X\<subseteq>G\<close>
+        have "A\<in>X \<Longrightarrow> countable(A)" for A
+          using Finite_imp_countable by auto
+        with \<open>|X| < \<aleph>\<^bsub>1\<^esub>\<close>
+        have "countable(\<Union>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 \<open>countable(_) \<Longrightarrow> countable({A \<in> G . _  \<inter> A \<noteq> 0})\<close>
+        have "countable({A \<in> G . (\<Union>X) \<inter> A \<noteq> 0})" .
+        with \<open>G \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
+        obtain B where "B\<in>G" "B \<notin> {A \<in> G . (\<Union>X) \<inter> A \<noteq> 0}" 
+          using nat_lt_Aleph1 cardinal_Card_eqpoll_iff[of "\<aleph>\<^bsub>1\<^esub>" G]
+            uncountable_not_subset_countable[of "{A \<in> G . (\<Union>X) \<inter> A \<noteq> 0}" G]
+            uncountable_iff_nat_lt_cardinal
+          by auto
+        then
+        show "\<exists>A\<in>G. \<forall>S\<in>X. S \<inter> A = 0" by auto
+      qed
+      moreover from \<open>G \<approx> \<aleph>\<^bsub>1\<^esub>\<close>
+      obtain b where "b\<in>G"
+        using uncountable_iff_subset_eqpoll_Aleph1
+          uncountable_not_empty by blast
+      ultimately
+      text\<open>Hence, the hypotheses to perform a bounded-cardinal selection
+      are satisfied,\<close>
+      obtain S where "S:\<aleph>\<^bsub>1\<^esub>\<rightarrow>G" "\<alpha>\<in>\<aleph>\<^bsub>1\<^esub> \<Longrightarrow> \<beta>\<in>\<aleph>\<^bsub>1\<^esub> \<Longrightarrow> \<alpha><\<beta> \<Longrightarrow> S`\<alpha> \<inter> S`\<beta> = 0"
+        for \<alpha> \<beta>
+        using bounded_cardinal_selection[of "\<aleph>\<^bsub>1\<^esub>" G "\<lambda>s a. s \<inter> a = 0" b]
+        by force
+      then
+      have "\<alpha> \<in> \<aleph>\<^bsub>1\<^esub> \<Longrightarrow> \<beta> \<in> \<aleph>\<^bsub>1\<^esub> \<Longrightarrow> \<alpha>\<noteq>\<beta> \<Longrightarrow> S`\<alpha> \<inter> S`\<beta> = 0" for \<alpha> \<beta>
+        using lt_neq_symmetry[of "\<aleph>\<^bsub>1\<^esub>" "\<lambda>\<alpha> \<beta>. S`\<alpha> \<inter> S`\<beta> = 0"] Card_is_Ord
+        by auto blast
+      text\<open>and a symmetry argument shows that obtained \<^term>\<open>S\<close> is
+      an injective  \<^term>\<open>\<aleph>\<^bsub>1\<^esub>\<close>-sequence of disjoint elements of \<^term>\<open>G\<close>.\<close>
+      moreover from this and \<open>\<And>A. A\<in>G \<Longrightarrow> |A| = succ(n)\<close> \<open>S : \<aleph>\<^bsub>1\<^esub> \<rightarrow> G\<close>
+      have "S \<in> inj(\<aleph>\<^bsub>1\<^esub>, G)"
+        using cardinal_succ_not_0 Int_eq_zero_imp_not_eq[of "\<aleph>\<^bsub>1\<^esub>" "\<lambda>x. S`x"]
+        unfolding inj_def by fastforce
+      moreover from calculation
+      have "range(S) \<approx> \<aleph>\<^bsub>1\<^esub>"
+        using inj_bij_range eqpoll_sym unfolding eqpoll_def by fast
+      moreover from calculation
+      have "range(S) \<subseteq> G"
+        using inj_is_fun range_fun_subset_codomain by fast
+      ultimately
+      show "\<exists>D. D \<subseteq> G \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
+        using inj_is_fun range_eq_image[of S "\<aleph>\<^bsub>1\<^esub>" G]
+          image_function[OF fun_is_function, OF inj_is_fun, of S "\<aleph>\<^bsub>1\<^esub>" G]
+          domain_of_fun[OF inj_is_fun, of S "\<aleph>\<^bsub>1\<^esub>" G]
+        by (rule_tac x="S``\<aleph>\<^bsub>1\<^esub>" in exI) auto
+      text\<open>This finishes the successor case and hence the proof.\<close>
+    qed
+  qed
+  with \<open>G \<subseteq> F\<close>
+  show ?thesis by blast
+qed
+
+lemma delta_system_uncountable:
+  assumes "\<forall>A\<in>F. Finite(A)" "uncountable(F)"
+  shows "\<exists>D. D \<subseteq> F \<and> delta_system(D) \<and> D \<approx> \<aleph>\<^bsub>1\<^esub>"
+proof -
+  from assms
+  obtain S where "S \<subseteq> F" "S \<approx> \<aleph>\<^bsub>1\<^esub>"
+    using uncountable_iff_subset_eqpoll_Aleph1[of F] by auto
+  moreover from \<open>\<forall>A\<in>F. Finite(A)\<close> and this
+  have "\<forall>A\<in>S. Finite(A)" by auto
+  ultimately
+  show ?thesis using delta_system_Aleph1[of S]
+    by auto
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Delta_System_Lemma/Konig.thy b/thys/Delta_System_Lemma/Konig.thy
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/Konig.thy
@@ -0,0 +1,187 @@
+theory Konig
+  imports
+    Cofinality
+    Cardinal_Library
+
+begin
+
+text\<open>Now, using the Axiom of choice, we can show that all successor
+cardinals are regular.\<close>
+
+lemma cf_csucc:
+  assumes "InfCard(z)"
+  shows "cf(z\<^sup>+) = z\<^sup>+"
+proof (rule ccontr)
+  assume "cf(z\<^sup>+) \<noteq> z\<^sup>+"
+  moreover from \<open>InfCard(z)\<close>
+  have "Ord(z\<^sup>+)" "Ord(z)" "Limit(z)" "Limit(z\<^sup>+)" "Card(z\<^sup>+)" "Card(z)"
+    using InfCard_csucc Card_is_Ord InfCard_is_Card InfCard_is_Limit
+    by fastforce+
+  moreover from calculation
+  have "cf(z\<^sup>+) < z\<^sup>+"
+    using cf_le_cardinal[of "z\<^sup>+", THEN le_iff[THEN iffD1]]
+      Card_cardinal_eq
+    by simp
+  ultimately
+  obtain G where "G:cf(z\<^sup>+)\<rightarrow> z\<^sup>+" "\<forall>\<beta>\<in>z\<^sup>+. \<exists>y\<in>cf(z\<^sup>+). \<beta> < G`y"
+    using Limit_cofinal_fun_lt[of "z\<^sup>+" _ "cf(z\<^sup>+)"] Ord_cf
+      cf_le_cf_fun[of "z\<^sup>+" "cf(z\<^sup>+)"] le_refl[of "cf(z\<^sup>+)"]
+    by auto
+  with \<open>Card(z)\<close> \<open>Card(z\<^sup>+)\<close> \<open>Ord(z\<^sup>+)\<close>
+  have "\<forall>\<beta>\<in>cf(z\<^sup>+). |G`\<beta>| \<le> z"
+    using apply_type[of G "cf(z\<^sup>+)" "\<lambda>_. z\<^sup>+", THEN ltI] Card_lt_iff[THEN iffD2]
+      Ord_in_Ord[OF Card_is_Ord, of "z\<^sup>+"] cardinal_lt_csucc_iff[THEN iffD1]
+    by auto
+  from \<open>cf(z\<^sup>+) < z\<^sup>+\<close> \<open>InfCard(z)\<close> \<open>Ord(z)\<close>
+  have "cf(z\<^sup>+) \<lesssim> z"
+    using cardinal_lt_csucc_iff[of "z" "cf(z\<^sup>+)"] Card_csucc[of "z"]
+      le_Card_iff[of "z" "cf(z\<^sup>+)"] InfCard_is_Card
+      Card_lt_iff[of "cf(z\<^sup>+)" "z\<^sup>+"] lt_Ord[of "cf(z\<^sup>+)" "z\<^sup>+"]
+    by simp
+  with \<open>cf(z\<^sup>+) < z\<^sup>+\<close> \<open>\<forall>\<beta>\<in>cf(z\<^sup>+). |G`\<beta>| \<le> _\<close> \<open>InfCard(z)\<close>
+  have "|\<Union>\<beta>\<in>cf(z\<^sup>+). G`\<beta>| \<le> z"
+    using InfCard_csucc[of z]
+      subset_imp_lepoll[THEN lepoll_imp_Card_le, of "\<Union>\<beta>\<in>cf(z\<^sup>+). G`\<beta>" "z"]
+    by (rule_tac leqpoll_imp_cardinal_UN_le) auto
+  moreover
+  note \<open>Ord(z)\<close>
+  moreover from \<open>\<forall>\<beta>\<in>z\<^sup>+. \<exists>y\<in>cf(z\<^sup>+). \<beta> < G`y\<close> and this
+  have "z\<^sup>+ \<subseteq> (\<Union>\<beta>\<in>cf(z\<^sup>+). G`\<beta>)"
+    by (blast dest:ltD)
+  ultimately
+  have "z\<^sup>+ \<le> z"
+    using subset_imp_le_cardinal[of "z\<^sup>+" "\<Union>\<beta>\<in>cf(z\<^sup>+). G`\<beta>"] le_trans
+      InfCard_is_Card Card_csucc[of z] Card_cardinal_eq
+    by auto
+  with \<open>Ord(z)\<close>
+  show "False"
+    using lt_csucc[of z] not_lt_iff_le[THEN iffD2, of z "z\<^sup>+"]
+      Card_csucc[THEN Card_is_Ord]
+    by auto
+qed
+
+text\<open>And this finishes the calculation of cofinality of Alephs.\<close>
+
+lemma cf_Aleph_succ: "Ord(z) \<Longrightarrow> cf(\<aleph>\<^bsub>succ(z)\<^esub>) = \<aleph>\<^bsub>succ(z)\<^esub>"
+  using Aleph_succ cf_csucc InfCard_Aleph by simp
+
+subsection\<open>König's Theorem\label{sec:konig}\<close>
+
+text\<open>We end this section by proving König's Theorem on the cofinality
+of cardinal exponentiation. This is a strengthening of Cantor's theorem
+and it is essentially the only basic way to prove strict cardinal
+inequalities.
+
+It is proved rather straightforwardly with the tools already developed.\<close>
+
+lemma konigs_theorem:
+  notes [dest] = InfCard_is_Card Card_is_Ord
+    and [trans] = lt_trans1 lt_trans2
+  assumes
+    "InfCard(\<kappa>)" "InfCard(\<nu>)" "cf(\<kappa>) \<le> \<nu>"
+  shows
+    "\<kappa> < \<kappa>\<^bsup>\<up>\<nu>\<^esup>"
+  using assms(1,2) Card_cexp
+proof (intro not_le_iff_lt[THEN iffD1] notI)
+  assume "\<kappa>\<^bsup>\<up>\<nu>\<^esup> \<le> \<kappa>"
+  moreover
+  note \<open>InfCard(\<kappa>)\<close>
+  moreover from calculation
+  have "\<nu> \<rightarrow> \<kappa> \<lesssim> \<kappa>"
+    using Card_cardinal_eq[OF InfCard_is_Card, symmetric]
+      Card_le_imp_lepoll
+    unfolding cexp_def by simp
+  ultimately
+  obtain G where "G \<in> surj(\<kappa>, \<nu> \<rightarrow> \<kappa>)"
+    using inj_imp_surj[OF _ function_space_nonempty,
+        OF _ nat_into_InfCard] by blast
+  from assms
+  obtain f where "f:\<nu> \<rightarrow> \<kappa>" "cf_fun(f,\<kappa>)"
+    using cf_le_cf_fun[OF _ InfCard_is_Limit] by blast
+  define H where "H(\<alpha>) \<equiv> \<mu> x. x\<in>\<kappa> \<and> (\<forall>m<f`\<alpha>. G`m`\<alpha> \<noteq> x)"
+    (is "_ \<equiv> \<mu> x. ?P(\<alpha>,x)") for \<alpha>
+  have H_satisfies: "?P(\<alpha>,H(\<alpha>))" if "\<alpha> \<in> \<nu>" for \<alpha>
+  proof -
+    obtain h where "?P(\<alpha>,h)"
+    proof -
+      from \<open>\<alpha>\<in>\<nu>\<close> \<open>f:\<nu> \<rightarrow> \<kappa>\<close> \<open>InfCard(\<kappa>)\<close>
+      have "f`\<alpha> < \<kappa>"
+        using apply_type[of _ _ "\<lambda>_ . \<kappa>"] by (auto intro:ltI)
+      have "|{G`m`\<alpha> . m \<in> {x\<in>\<kappa> . x < f`\<alpha>}}| \<le> |{x\<in>\<kappa> . x < f`\<alpha>}|"
+        using cardinal_RepFun_le by simp
+      also from \<open>f`\<alpha> < \<kappa>\<close> \<open>InfCard(\<kappa>)\<close>
+      have "|{x\<in>\<kappa> . x < f`\<alpha>}| < |\<kappa>|"
+        using Card_lt_iff[OF lt_Ord, THEN iffD2, of "f`\<alpha>" \<kappa> \<kappa>]
+          Ord_eq_Collect_lt[of "f`\<alpha>" \<kappa>] Card_cardinal_eq
+        by force
+      finally
+      have "|{G`m`\<alpha> . m \<in> {x\<in>\<kappa> . x < f`\<alpha>}}| < |\<kappa>|" .
+      moreover from \<open>f`\<alpha> < \<kappa>\<close> \<open>InfCard(\<kappa>)\<close>
+      have "m<f`\<alpha> \<Longrightarrow> m\<in>\<kappa>" for m
+        using Ord_trans[of m "f`\<alpha>" \<kappa>]
+        by (auto dest:ltD)
+      ultimately
+      have "\<exists>h. ?P(\<alpha>,h)"
+        using lt_cardinal_imp_not_subset by blast
+      with that
+      show ?thesis by blast
+    qed
+    with assms
+    show "?P(\<alpha>,H(\<alpha>))"
+      using LeastI[of "?P(\<alpha>)" h] lt_Ord Ord_in_Ord
+      unfolding H_def by fastforce
+  qed
+  then
+  have "(\<lambda>\<alpha>\<in>\<nu>. H(\<alpha>)): \<nu> \<rightarrow> \<kappa>"
+    using lam_type by auto
+  with \<open>G \<in> surj(\<kappa>, \<nu> \<rightarrow> \<kappa>)\<close>
+  obtain n where "n\<in>\<kappa>" "G`n = (\<lambda>\<alpha>\<in>\<nu>. H(\<alpha>))"
+    unfolding surj_def by blast
+  moreover
+  note \<open>InfCard(\<kappa>)\<close> \<open>f: \<nu> \<rightarrow> \<kappa>\<close> \<open>cf_fun(f,_)\<close>
+  ultimately
+  obtain \<alpha> where "n < f`\<alpha>" "\<alpha>\<in>\<nu>"
+    using Limit_cofinal_fun_lt[OF InfCard_is_Limit] by blast
+  moreover from calculation and \<open>G`n = (\<lambda>\<alpha>\<in>\<nu>. H(\<alpha>))\<close>
+  have "G`n`\<alpha> = H(\<alpha>)"
+    using ltD by simp
+  moreover from calculation and H_satisfies
+  have "\<forall>m<f`\<alpha>. G`m`\<alpha> \<noteq> H(\<alpha>)" by simp
+  ultimately
+  show "False" by blast
+qed blast+
+
+lemma cf_cexp:
+  assumes
+    "Card(\<kappa>)" "InfCard(\<nu>)" "2 \<le> \<kappa>"
+  shows
+    "\<nu> < cf(\<kappa>\<^bsup>\<up>\<nu>\<^esup>)"
+proof (rule ccontr)
+  assume "\<not> \<nu> < cf(\<kappa>\<^bsup>\<up>\<nu>\<^esup>)"
+  with \<open>InfCard(\<nu>)\<close>
+  have "cf(\<kappa>\<^bsup>\<up>\<nu>\<^esup>) \<le> \<nu>" 
+    using not_lt_iff_le Ord_cf InfCard_is_Card Card_is_Ord by simp
+  moreover
+  note assms
+  moreover from calculation
+  have "InfCard(\<kappa>\<^bsup>\<up>\<nu>\<^esup>)" using InfCard_cexp by simp
+  moreover from calculation
+  have "\<kappa>\<^bsup>\<up>\<nu>\<^esup> < (\<kappa>\<^bsup>\<up>\<nu>\<^esup>)\<^bsup>\<up>\<nu>\<^esup>" 
+    using konigs_theorem by simp
+  ultimately
+  show "False" using cexp_cexp_cmult InfCard_csquare_eq by auto
+qed
+
+text\<open>Finally, the next two corollaries illustrate the only possible
+exceptions to the value of the cardinality of the continuum: The limit
+cardinals of countable cofinality. That these are the only exceptions
+is a consequence of Easton's Theorem~\cite[Thm 15.18]{Jech_Millennium}.\<close>
+
+corollary cf_continuum: "\<aleph>\<^bsub>0\<^esub> < cf(2\<^bsup>\<up>\<aleph>\<^bsub>0\<^esub>\<^esup>)"
+  using cf_cexp InfCard_Aleph nat_into_Card by simp
+
+corollary continuum_not_eq_Aleph_nat: "2\<^bsup>\<up>\<aleph>\<^bsub>0\<^esub>\<^esup> \<noteq> \<aleph>\<^bsub>\<omega>\<^esub>"
+  using cf_continuum cf_Aleph_Limit[OF Limit_nat] cf_nat
+    Aleph_zero_eq_nat by auto
+
+end
\ No newline at end of file
diff --git a/thys/Delta_System_Lemma/ROOT b/thys/Delta_System_Lemma/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/ROOT
@@ -0,0 +1,23 @@
+chapter AFP
+
+session Delta_System_Lemma (AFP) =  "ZF-Constructible" +
+  description "
+    Cofinality and Delta System Lemma
+
+    We formalize the basic results on cofinality of linearly ordered
+    sets and ordinals and Shanin's Lemma for uncountable families of
+    finite sets. This last result is used to prove the countable chain
+    condition for Cohen posets. We work in the set theory framework of
+    Isabelle/ZF, using the Axiom of Choice as needed.
+  "
+  options [timeout = 600]
+  theories
+    "Konig"
+    "Delta_System"
+    "Cohen_Posets"
+  document_files
+    "root.tex"
+    "header-delta-system.tex"
+    "multidef.sty"
+    "root.bib"
+    "root.bst"
diff --git a/thys/Delta_System_Lemma/ZF_Library.thy b/thys/Delta_System_Lemma/ZF_Library.thy
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/ZF_Library.thy
@@ -0,0 +1,996 @@
+section\<open>Library of basic $\ZF$ results\label{sec:zf-lib}\<close>
+
+theory ZF_Library
+  imports
+    "ZF-Constructible.Normal"
+
+begin
+
+text\<open>This theory gathers basic ``combinatorial'' results that can be proved
+in $\ZF$ (that is, without using the Axiom of Choice $\AC$).
+\<close>
+
+text\<open>We begin by setting up math-friendly notation.\<close>
+
+no_notation oadd (infixl \<open>++\<close> 65)
+no_notation sum (infixr \<open>+\<close> 65)
+notation oadd (infixl \<open>+\<close> 65)
+notation nat (\<open>\<omega>\<close>)
+notation csucc (\<open>_\<^sup>+\<close> [90])
+no_notation Aleph (\<open>\<aleph>_\<close> [90] 90)
+notation Aleph (\<open>\<aleph>\<^bsub>_\<^esub>\<close>)
+syntax "_ge"  :: "[i,i] \<Rightarrow> o"  (infixl \<open>\<ge>\<close> 50)
+translations "x \<ge> y" \<rightharpoonup> "y \<le> x"
+
+
+subsection\<open>Some minimal arithmetic/ordinal stuff\<close>
+
+lemma Un_leD1 : "i \<union> j \<le> k \<Longrightarrow> Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> Ord(k) \<Longrightarrow> i \<le> k"
+  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)
+
+lemma Un_leD2 : "i \<union> j \<le> k \<Longrightarrow> Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> Ord(k) \<Longrightarrow> j \<le> k"
+  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)
+
+lemma Un_memD1: "i \<union> j \<in> k \<Longrightarrow> Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> Ord(k) \<Longrightarrow> i \<le> k"
+  by (drule ltI, assumption, drule leI, rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)
+
+lemma Un_memD2 : "i \<union> j \<in> k \<Longrightarrow> Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> Ord(k) \<Longrightarrow> j \<le> k"
+  by (drule ltI, assumption, drule leI, rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)
+
+text\<open>This lemma allows to apply arithmetic simprocs to ordinal addition\<close>
+lemma nat_oadd_add[simp]:
+  assumes "m \<in> \<omega>" "n \<in> \<omega>" shows "n + m = n #+ m"
+  using assms
+  by induct simp_all
+
+lemma Ord_has_max_imp_succ:
+  assumes "Ord(\<gamma>)" "\<beta> \<in> \<gamma>" "\<forall>\<alpha>\<in>\<gamma>. \<alpha> \<le> \<beta>"
+  shows "\<gamma> = succ(\<beta>)"
+  using assms Ord_trans[of _ \<beta> \<gamma>]
+  unfolding lt_def
+  by (intro equalityI subsetI) auto
+
+lemma Least_antitone:
+  assumes
+    "Ord(j)" "P(j)" "\<And>i. P(i) \<Longrightarrow> Q(i)"
+  shows
+    "(\<mu> i. Q(i)) \<le> (\<mu> i. P(i))"
+  using assms LeastI2[of P j Q] Least_le by simp
+
+lemma Least_set_antitone:
+  "Ord(j) \<Longrightarrow> j\<in>A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<mu> i. i\<in>B) \<le> (\<mu> i. i\<in>A)"
+  using subset_iff by (auto intro:Least_antitone)
+
+lemma le_neq_imp_lt:
+  "x\<le>y \<Longrightarrow> x\<noteq>y \<Longrightarrow> x<y"
+  using ltD ltI[of x y] le_Ord2
+  unfolding succ_def by auto
+
+text\<open>Strict upper bound of a set of ordinals.\<close>
+definition
+  str_bound :: "i\<Rightarrow>i" where
+  "str_bound(A) \<equiv> \<Union>a\<in>A. succ(a)"
+
+lemma str_bound_type [TC]: "\<forall>a\<in>A. Ord(a) \<Longrightarrow> Ord(str_bound(A))"
+  unfolding str_bound_def by auto
+
+lemma str_bound_lt: "\<forall>a\<in>A. Ord(a) \<Longrightarrow> \<forall>a\<in>A. a < str_bound(A)"
+  unfolding str_bound_def using str_bound_type
+  by (blast intro:ltI)
+
+lemma naturals_lt_nat[intro]: "n \<in> \<omega> \<Longrightarrow> n < \<omega>"
+  unfolding lt_def by simp
+
+text\<open>The next two lemmas are handy when one is constructing
+some object recursively. The first handles injectivity (of recursively
+constructed sequences of sets), while the second is helpful for
+establishing a symmetry argument.\<close>
+lemma Int_eq_zero_imp_not_eq:
+  assumes
+    "\<And>x y. x\<in>D \<Longrightarrow> y \<in> D \<Longrightarrow> x \<noteq> y \<Longrightarrow> A(x) \<inter> A(y) = 0"
+    "\<And>x. x\<in>D \<Longrightarrow> A(x) \<noteq> 0" "a\<in>D" "b\<in>D" "a\<noteq>b"
+  shows
+    "A(a) \<noteq> A(b)"
+  using assms by fastforce
+
+lemma lt_neq_symmetry:
+  assumes
+    "\<And>\<alpha> \<beta>. \<alpha> \<in> \<gamma> \<Longrightarrow> \<beta> \<in> \<gamma> \<Longrightarrow> \<alpha> < \<beta> \<Longrightarrow> Q(\<alpha>,\<beta>)"
+    "\<And>\<alpha> \<beta>. Q(\<alpha>,\<beta>) \<Longrightarrow> Q(\<beta>,\<alpha>)"
+    "\<alpha> \<in> \<gamma>" "\<beta> \<in> \<gamma>" "\<alpha> \<noteq> \<beta>"
+    "Ord(\<gamma>)"
+  shows
+    "Q(\<alpha>,\<beta>)"
+proof -
+  from assms
+  consider "\<alpha><\<beta>" | "\<beta><\<alpha>"
+    using Ord_linear_lt[of \<alpha> \<beta> thesis] Ord_in_Ord[of \<gamma>]
+    by auto
+  then
+  show ?thesis by cases (auto simp add:assms)
+qed
+
+lemma cardinal_succ_not_0: "|A| = succ(n) \<Longrightarrow> A \<noteq> 0"
+  by auto
+
+lemma Ord_eq_Collect_lt: "i<\<alpha> \<Longrightarrow> {j\<in>\<alpha>. j<i} = i"
+  \<comment> \<open>almost the same proof as @{thm nat_eq_Collect_lt}\<close>
+  apply (rule equalityI)
+  apply (blast dest: ltD)
+  apply (auto simp add: Ord_mem_iff_lt)
+  apply (rule Ord_trans ltI[OF _ lt_Ord]; auto simp add:lt_def dest:ltD)+
+  done
+
+
+subsection\<open>Manipulation of function spaces\<close>
+
+definition
+  Finite_to_one :: "[i,i] \<Rightarrow> i" where
+  "Finite_to_one(X,Y) \<equiv> {f:X\<rightarrow>Y. \<forall>y\<in>Y. Finite({x\<in>X . f`x = y})}"
+
+lemma Finite_to_oneI[intro]:
+  assumes "f:X\<rightarrow>Y" "\<And>y. y\<in>Y \<Longrightarrow> Finite({x\<in>X . f`x = y})"
+  shows "f \<in> Finite_to_one(X,Y)"
+  using assms unfolding Finite_to_one_def by simp
+
+lemma Finite_to_oneD[dest]:
+  "f \<in> Finite_to_one(X,Y) \<Longrightarrow> f:X\<rightarrow>Y"
+  "f \<in> Finite_to_one(X,Y) \<Longrightarrow> y\<in>Y \<Longrightarrow>  Finite({x\<in>X . f`x = y})"
+  unfolding Finite_to_one_def by simp_all
+
+lemma subset_Diff_Un: "X \<subseteq> A \<Longrightarrow> A = (A - X) \<union> X " by auto
+
+lemma Diff_bij:
+  assumes "\<forall>A\<in>F. X \<subseteq> A" shows "(\<lambda>A\<in>F. A-X) \<in> bij(F, {A-X. A\<in>F})"
+  using assms unfolding bij_def inj_def surj_def
+  by (auto intro:lam_type, subst subset_Diff_Un[of X]) auto
+
+lemma function_space_nonempty:
+  assumes "b\<in>B"
+  shows "(\<lambda>x\<in>A. b) : A \<rightarrow> B"
+  using assms lam_type by force
+
+lemma vimage_lam: "(\<lambda>x\<in>A. f(x)) -`` B = { x\<in>A . f(x) \<in> B }"
+  using lam_funtype[of A f, THEN [2] domain_type]
+    lam_funtype[of A f, THEN [2] apply_equality] lamI[of _ A f]
+  by auto blast
+
+lemma range_fun_subset_codomain:
+  assumes "h:B \<rightarrow> C"
+  shows "range(h) \<subseteq> C"
+  unfolding range_def domain_def converse_def using range_type[OF _ assms]  by auto
+
+lemma Pi_rangeD:
+  assumes "f\<in>Pi(A,B)" "b \<in> range(f)"
+  shows "\<exists>a\<in>A. f`a = b"
+  using assms apply_equality[OF _ assms(1), of _ b]
+    domain_type[OF _ assms(1)] by auto
+
+lemma Pi_range_eq: "f \<in> Pi(A,B) \<Longrightarrow> range(f) = {f ` x . x \<in> A}"
+  using Pi_rangeD[of f A B] apply_rangeI[of f A B]
+  by blast
+
+lemma Pi_vimage_subset : "f \<in> Pi(A,B) \<Longrightarrow> f-``C \<subseteq> A"
+  unfolding Pi_def by auto
+
+lemma apply_in_range:
+  assumes
+    "Ord(\<gamma>)" "\<gamma>\<noteq>0" "f: A \<rightarrow> \<gamma>"
+  shows
+    "f`x\<in>\<gamma>"
+proof (cases "x\<in>A")
+  case True
+  from assms \<open>x\<in>A\<close>
+  show ?thesis
+    using   domain_of_fun apply_rangeI  by simp
+next
+  case False
+  from assms \<open>x\<notin>A\<close>
+  show ?thesis
+    using apply_0 Ord_0_lt ltD domain_of_fun by auto
+qed
+
+lemma range_eq_image:
+  assumes "f:A\<rightarrow>B"
+  shows "range(f) = f``A"
+proof
+  show "f `` A \<subseteq> range(f)"
+    unfolding image_def by blast
+  {
+    fix x
+    assume "x\<in>range(f)"
+    with assms
+    have "x\<in>f``A"
+      using domain_of_fun[of f A "\<lambda>_. B"] by auto
+  }
+  then
+  show "range(f) \<subseteq> f `` A" ..
+qed
+
+lemma Image_sub_codomain: "f:A\<rightarrow>B \<Longrightarrow> f``C \<subseteq> B"
+  using image_subset fun_is_rel[of _ _ "\<lambda>_ . B"] by force
+
+lemma inj_to_Image:
+  assumes
+    "f:A\<rightarrow>B" "f \<in> inj(A,B)"
+  shows
+    "f \<in> inj(A,f``A)"
+  using assms inj_inj_range range_eq_image by force
+
+lemma inj_imp_surj:
+  fixes f b
+  notes inj_is_fun[dest]
+  defines [simp]: "ifx(x) \<equiv> if x\<in>range(f) then converse(f)`x else b"
+  assumes "f \<in> inj(B,A)" "b\<in>B"
+  shows "(\<lambda>x\<in>A. ifx(x)) \<in> surj(A,B)"
+proof -
+  from assms
+  have "converse(f) \<in> surj(range(f),B)" "range(f) \<subseteq> A"
+    "converse(f) : range(f) \<rightarrow> B"
+    using inj_converse_surj range_fun_subset_codomain surj_is_fun by blast+
+  with \<open>b\<in>B\<close>
+  show "(\<lambda>x\<in>A. ifx(x)) \<in> surj(A,B)"
+    unfolding surj_def
+  proof (intro CollectI lam_type ballI; elim CollectE)
+    fix y
+    assume "y \<in> B" "\<forall>y\<in>B. \<exists>x\<in>range(f). converse(f) ` x = y"
+    with \<open>range(f) \<subseteq> A\<close>
+    show "\<exists>x\<in>A. (\<lambda>x\<in>A. ifx(x)) ` x = y"
+      by (drule_tac bspec, auto)
+  qed simp
+qed
+
+lemma fun_Pi_disjoint_Un:
+  assumes "f \<in> Pi(A,B)" "g \<in> Pi(C,D)"  "A \<inter> C = 0"
+  shows "f \<union> g \<in> Pi(A \<union> C, \<lambda>x. B(x) \<union> D(x))"
+  using assms
+  by (simp add: Pi_iff extension Un_rls) (unfold function_def, blast)
+
+lemma Un_restrict_decomposition:
+  assumes "f \<in> Pi(A,B)"
+  shows "f = restrict(f, A \<inter> C) \<union> restrict(f, A - C)"
+  using assms
+proof (rule fun_extension)
+  from assms
+  have "restrict(f,A\<inter>C) \<union> restrict(f,A-C) \<in> Pi(A\<inter>C \<union> (A-C), \<lambda>x. B(x)\<union>B(x))"
+    using restrict_type2[of f A B]
+    by (rule_tac fun_Pi_disjoint_Un) force+
+  moreover
+  have "(A \<inter> C) \<union> (A - C) = A" by auto
+  ultimately
+  show "restrict(f, A \<inter> C) \<union> restrict(f, A - C) \<in> Pi(A, B)" by simp
+next
+  fix x
+  assume "x \<in> A"
+  with assms
+  show "f ` x = (restrict(f, A \<inter> C) \<union> restrict(f, A - C)) ` x"
+    using restrict fun_disjoint_apply1[of _ "restrict(f,_)"]
+      fun_disjoint_apply2[of _ "restrict(f,_)"]
+      domain_restrict[of f] apply_0 domain_of_fun
+    by (cases "x\<in>C") simp_all
+qed
+
+lemma restrict_eq_imp_Un_into_Pi:
+  assumes "f \<in> Pi(A,B)" "g \<in> Pi(C,D)" "restrict(f, A \<inter> C) = restrict(g, A \<inter> C)"
+  shows "f \<union> g \<in> Pi(A \<union> C, \<lambda>x. B(x) \<union> D(x))"
+proof -
+  note assms
+  moreover from this
+  have "x \<notin> g \<Longrightarrow> x \<notin> restrict(g, A \<inter> C)" for x
+    using restrict_subset[of g "A \<inter> C"] by auto
+  moreover from calculation
+  have "x \<in> f \<Longrightarrow> x \<in> restrict(f, A - C) \<or> x \<in> restrict(g, A \<inter> C)" for x
+    by (subst (asm) Un_restrict_decomposition[of f A B "C"]) auto
+  ultimately
+  have "f \<union> g = restrict(f, A - C) \<union> g"
+    using restrict_subset[of g "A \<inter> C"]
+    by (subst Un_restrict_decomposition[of f A B "C"]) auto
+  moreover
+  have "A - C \<union> C = A \<union> C" by auto
+  moreover
+  note assms
+  ultimately
+  show ?thesis
+    using fun_Pi_disjoint_Un[OF
+        restrict_type2[of f A B "A-C"], of g C D]
+    by auto
+qed
+
+lemma restrict_eq_imp_Un_into_Pi':
+  assumes "f \<in> Pi(A,B)" "g \<in> Pi(C,D)"
+    "restrict(f, domain(f) \<inter> domain(g)) = restrict(g, domain(f) \<inter> domain(g))"
+  shows "f \<union> g \<in> Pi(A \<union> C, \<lambda>x. B(x) \<union> D(x))"
+  using  assms domain_of_fun restrict_eq_imp_Un_into_Pi by simp
+
+lemma restrict_subset_Sigma: "f \<subseteq> Sigma(C,B) \<Longrightarrow> restrict(f,A) \<subseteq> Sigma(A\<inter>C, B)"
+  by (auto simp add: restrict_def)
+
+
+subsection\<open>Finite sets\<close>
+
+lemma Replace_sing1:
+  "\<lbrakk> (\<exists>a. P(d,a)) \<and> (\<forall>y y'. P(d,y) \<longrightarrow> P(d,y') \<longrightarrow> y=y') \<rbrakk> \<Longrightarrow> \<exists>a. {y . x \<in> {d}, P(x,y)} = {a}"
+  by blast
+
+\<comment> \<open>Not really necessary\<close>
+lemma Replace_sing2:
+  assumes "\<forall>a. \<not> P(d,a)"
+  shows "{y . x \<in> {d}, P(x,y)} = 0"
+  using assms by auto
+
+lemma Replace_sing3:
+  assumes "\<exists>c e. c \<noteq> e \<and> P(d,c) \<and> P(d,e)"
+  shows "{y . x \<in> {d}, P(x,y)} = 0"
+proof -
+  {
+    fix z
+    {
+      assume "\<forall>y. P(d, y) \<longrightarrow> y = z"
+      with assms
+      have "False" by auto
+    }
+    then
+    have "z \<notin> {y . x \<in> {d}, P(x,y)}"
+      using Replace_iff by auto
+  }
+  then
+  show ?thesis
+    by (intro equalityI subsetI) simp_all
+qed
+
+lemma Replace_Un: "{b . a \<in> A \<union> B, Q(a, b)} =
+        {b . a \<in> A, Q(a, b)} \<union> {b . a \<in> B, Q(a, b)}"
+  by (intro equalityI subsetI) (auto simp add:Replace_iff)
+
+lemma Replace_subset_sing: "\<exists>z. {y . x \<in> {d}, P(x,y)} \<subseteq> {z}"
+proof -
+  consider
+    (1) "(\<exists>a. P(d,a)) \<and> (\<forall>y y'. P(d,y) \<longrightarrow> P(d,y') \<longrightarrow> y=y')" |
+    (2) "\<forall>a. \<not> P(d,a)" | (3) "\<exists>c e. c \<noteq> e \<and> P(d,c) \<and> P(d,e)" by auto
+  then
+  show "\<exists>z. {y . x \<in> {d}, P(x,y)} \<subseteq> {z}"
+  proof (cases)
+    case 1
+    then show ?thesis using Replace_sing1[of P d] by auto
+  next
+    case 2
+    then show ?thesis by auto
+  next
+    case 3
+    then show ?thesis using Replace_sing3[of P d] by auto
+  qed
+qed
+
+lemma Finite_Replace: "Finite(A) \<Longrightarrow> Finite(Replace(A,Q))"
+proof (induct rule:Finite_induct)
+  case 0
+  then
+  show ?case by simp
+next
+  case (cons x B)
+  moreover
+  have "{b . a \<in> cons(x, B), Q(a, b)} =
+        {b . a \<in> B, Q(a, b)} \<union> {b . a \<in> {x}, Q(a, b)}"
+    using Replace_Un unfolding cons_def by auto
+  moreover
+  obtain d where "{b . a \<in> {x}, Q(a, b)} \<subseteq> {d}"
+    using Replace_subset_sing[of _ Q] by blast
+  moreover from this
+  have "Finite({b . a \<in> {x}, Q(a, b)})"
+    using subset_Finite by simp
+  ultimately
+  show ?case using subset_Finite by simp
+qed
+
+lemma Finite_domain: "Finite(A) \<Longrightarrow> Finite(domain(A))"
+  using Finite_Replace unfolding domain_def
+  by auto
+
+lemma Finite_converse: "Finite(A) \<Longrightarrow> Finite(converse(A))"
+  using Finite_Replace unfolding converse_def
+  by auto
+
+lemma Finite_range: "Finite(A) \<Longrightarrow> Finite(range(A))"
+  using Finite_domain Finite_converse unfolding range_def
+  by blast
+
+lemma Finite_Sigma: "Finite(A) \<Longrightarrow> \<forall>x. Finite(B(x)) \<Longrightarrow> Finite(Sigma(A,B))"
+  unfolding Sigma_def using Finite_RepFun Finite_Union
+  by simp
+
+lemma Finite_Pi: "Finite(A) \<Longrightarrow> \<forall>x. Finite(B(x)) \<Longrightarrow> Finite(Pi(A,B))"
+  using Finite_Sigma
+    Finite_Pow subset_Finite[of "Pi(A,B)" "Pow(Sigma(A,B))"]
+  unfolding Pi_def
+  by auto
+
+
+subsection\<open>Basic results on equipollence, cardinality and related concepts\<close>
+
+lemma lepollD[dest]: "A \<lesssim> B \<Longrightarrow> \<exists>f. f \<in> inj(A, B)"
+  unfolding lepoll_def .
+
+lemma lepollI[intro]: "f \<in> inj(A, B) \<Longrightarrow> A \<lesssim> B"
+  unfolding lepoll_def by blast
+
+lemma eqpollD[dest]: "A \<approx> B \<Longrightarrow> \<exists>f. f \<in> bij(A, B)"
+  unfolding eqpoll_def .
+
+declare bij_imp_eqpoll[intro]
+
+lemma range_of_subset_eqpoll:
+  assumes "f \<in> inj(X,Y)" "S \<subseteq> X"
+  shows "S \<approx> f `` S"
+  using assms restrict_bij by blast
+
+text\<open>I thank Miguel Pagano for this proof.\<close>
+lemma function_space_eqpoll_cong:
+  assumes
+    "A \<approx> A'" "B \<approx> B'"
+  shows
+    "A \<rightarrow> B \<approx> A' \<rightarrow> B'"
+proof -
+  from assms(1)[THEN eqpoll_sym] assms(2)
+  obtain f g where "f \<in> bij(A',A)" "g \<in> bij(B,B')"
+    by blast
+  then
+  have "converse(g) : B' \<rightarrow> B" "converse(f): A \<rightarrow> A'"
+    using bij_converse_bij bij_is_fun by auto
+  show ?thesis
+    unfolding eqpoll_def
+  proof (intro exI fg_imp_bijective, rule_tac [1-2] lam_type)
+    fix F
+    assume "F: A \<rightarrow> B"
+    with \<open>f \<in> bij(A',A)\<close> \<open>g \<in> bij(B,B')\<close>
+    show "g O F O f : A' \<rightarrow> B'"
+      using bij_is_fun comp_fun by blast
+  next
+    fix F
+    assume "F: A' \<rightarrow> B'"
+    with \<open>converse(g) : B' \<rightarrow> B\<close> \<open>converse(f): A \<rightarrow> A'\<close>
+    show "converse(g) O F O converse(f) : A \<rightarrow> B"
+      using comp_fun by blast
+  next
+    from \<open>f\<in>_\<close> \<open>g\<in>_\<close> \<open>converse(f)\<in>_\<close> \<open>converse(g)\<in>_\<close>
+    have "(\<And>x. x \<in> A' \<rightarrow> B' \<Longrightarrow> converse(g) O x O converse(f) \<in> A \<rightarrow> B)"
+      using bij_is_fun comp_fun by blast
+    then
+    have "(\<lambda>x\<in>A \<rightarrow> B. g O x O f) O (\<lambda>x\<in>A' \<rightarrow> B'. converse(g) O x O converse(f))
+          =  (\<lambda>x\<in>A' \<rightarrow> B' . (g O converse(g)) O x O (converse(f) O f))"
+      using lam_cong comp_assoc comp_lam[of "A' \<rightarrow> B'" ] by auto
+    also
+    have "... = (\<lambda>x\<in>A' \<rightarrow> B' . id(B') O x O (id(A')))"
+      using left_comp_inverse[OF bij_is_inj[OF \<open>f\<in>_\<close>]]
+        right_comp_inverse[OF bij_is_surj[OF \<open>g\<in>_\<close>]]
+      by auto
+    also
+    have "... = (\<lambda>x\<in>A' \<rightarrow> B' . x)"
+      using left_comp_id[OF fun_is_rel] right_comp_id[OF fun_is_rel]  lam_cong by auto
+    also
+    have "... = id(A'\<rightarrow>B')" unfolding id_def by simp
+    finally
+    show "(\<lambda>x\<in>A -> B. g O x O f) O (\<lambda>x\<in>A' -> B'. converse(g) O x O converse(f)) = id(A' -> B')" .
+  next
+    from \<open>f\<in>_\<close> \<open>g\<in>_\<close>
+    have "(\<And>x. x \<in> A \<rightarrow> B \<Longrightarrow> g O x O f \<in> A' \<rightarrow> B')"
+      using bij_is_fun comp_fun by blast
+    then
+    have "(\<lambda>x\<in>A' -> B'. converse(g) O x O converse(f)) O (\<lambda>x\<in>A -> B. g O x O f)
+          = (\<lambda>x\<in>A \<rightarrow> B . (converse(g) O g) O x O (f O converse(f)))"
+      using comp_lam comp_assoc by auto
+    also
+    have "... = (\<lambda>x\<in>A \<rightarrow> B . id(B) O x O (id(A)))"
+      using
+        right_comp_inverse[OF bij_is_surj[OF \<open>f\<in>_\<close>]]
+        left_comp_inverse[OF bij_is_inj[OF \<open>g\<in>_\<close>]] lam_cong
+      by auto
+    also
+    have "... = (\<lambda>x\<in>A \<rightarrow> B . x)"
+      using left_comp_id[OF fun_is_rel] right_comp_id[OF fun_is_rel] lam_cong by auto
+    also
+    have "... = id(A\<rightarrow>B)" unfolding id_def by simp
+    finally
+    show "(\<lambda>x\<in>A' \<rightarrow> B'. converse(g) O x O converse(f)) O (\<lambda>x\<in>A -> B. g O x O f) = id(A -> B)" .
+  qed
+qed
+
+lemma curry_eqpoll:
+  fixes d \<nu>1 \<nu>2  \<kappa>
+  shows "\<nu>1 \<rightarrow> \<nu>2 \<rightarrow> \<kappa> \<approx> \<nu>1 \<times> \<nu>2 \<rightarrow> \<kappa>"
+  unfolding eqpoll_def
+proof (intro exI, rule lam_bijective,
+    rule_tac [1-2] lam_type, rule_tac [2] lam_type)
+  fix f z
+  assume "f : \<nu>1 \<rightarrow> \<nu>2 \<rightarrow> \<kappa>" "z \<in> \<nu>1 \<times> \<nu>2"
+  then
+  show "f`fst(z)`snd(z) \<in> \<kappa>"
+    by simp
+next
+  fix f x y
+  assume "f : \<nu>1 \<times> \<nu>2 \<rightarrow> \<kappa>" "x\<in>\<nu>1" "y\<in>\<nu>2"
+  then
+  show "f`\<langle>x,y\<rangle> \<in> \<kappa>" by simp
+next \<comment> \<open>one composition is the identity:\<close>
+  fix f
+  assume "f : \<nu>1 \<times> \<nu>2 \<rightarrow> \<kappa>"
+  then
+  show "(\<lambda>x\<in>\<nu>1 \<times> \<nu>2. (\<lambda>x\<in>\<nu>1. \<lambda>xa\<in>\<nu>2. f ` \<langle>x, xa\<rangle>) ` fst(x) ` snd(x)) = f"
+    by (auto intro:fun_extension)
+qed simp \<comment> \<open>the other composition follows automatically\<close>
+
+lemma Pow_eqpoll_function_space:
+  fixes d X
+  notes bool_of_o_def [simp]
+  defines [simp]:"d(A) \<equiv> (\<lambda>x\<in>X. bool_of_o(x\<in>A))"
+    \<comment> \<open>the witnessing map for the thesis:\<close>
+  shows "Pow(X) \<approx> X \<rightarrow> 2"
+  unfolding eqpoll_def
+proof (intro exI, rule lam_bijective)
+  \<comment> \<open>We give explicit mutual inverses\<close>
+  fix A
+  assume "A\<in>Pow(X)"
+  then
+  show "d(A) : X \<rightarrow> 2"
+    using lam_type[of _ "\<lambda>x. bool_of_o(x\<in>A)" "\<lambda>_. 2"]
+    by force
+  from \<open>A\<in>Pow(X)\<close>
+  show "{y\<in>X. d(A)`y = 1} = A"
+    by (auto)
+next
+  fix f
+  assume "f: X\<rightarrow>2"
+  then
+  show "d({y \<in> X . f ` y = 1}) = f"
+    using apply_type[OF \<open>f: X\<rightarrow>2\<close>]
+    by (force intro:fun_extension)
+qed blast
+
+lemma cantor_inj: "f \<notin> inj(Pow(A),A)"
+  using inj_imp_surj[OF _ Pow_bottom] cantor_surj by blast
+
+definition
+  cexp :: "[i,i] \<Rightarrow> i" ("_\<^bsup>\<up>_\<^esup>" [76,1] 75) where
+  "\<kappa>\<^bsup>\<up>\<nu>\<^esup> \<equiv> |\<nu> \<rightarrow> \<kappa>|"
+
+lemma Card_cexp: "Card(\<kappa>\<^bsup>\<up>\<nu>\<^esup>)"
+  unfolding cexp_def Card_cardinal by simp
+
+lemma eq_csucc_ord:
+  "Ord(i) \<Longrightarrow> i\<^sup>+ = |i|\<^sup>+"
+  using Card_lt_iff Least_cong unfolding csucc_def by auto
+
+text\<open>I thank Miguel Pagano for this proof.\<close>
+lemma lesspoll_csucc:
+  assumes "Ord(\<kappa>)"
+  shows "d \<prec> \<kappa>\<^sup>+ \<longleftrightarrow> d \<lesssim> \<kappa>"
+proof
+  assume "d \<prec> \<kappa>\<^sup>+"
+  moreover
+  note Card_is_Ord \<open>Ord(\<kappa>)\<close>
+  moreover from calculation
+  have "\<kappa> < \<kappa>\<^sup>+" "Card(\<kappa>\<^sup>+)"
+    using Ord_cardinal_eqpoll csucc_basic by simp_all
+  moreover from calculation
+  have "d \<prec> |\<kappa>|\<^sup>+" "Card(|\<kappa>|)" "d \<approx> |d|"
+    using eq_csucc_ord[of \<kappa>] lesspoll_imp_eqpoll eqpoll_sym by simp_all
+  moreover from calculation
+  have "|d| < |\<kappa>|\<^sup>+"
+    using lesspoll_cardinal_lt csucc_basic by simp
+  moreover from calculation
+  have "|d| \<lesssim> |\<kappa>|"
+    using Card_lt_csucc_iff le_imp_lepoll by simp
+  moreover from calculation
+  have "|d| \<lesssim> \<kappa>"
+    using lepoll_eq_trans Ord_cardinal_eqpoll by simp
+  ultimately
+  show "d \<lesssim> \<kappa>"
+    using eq_lepoll_trans by simp
+next
+  from \<open>Ord(\<kappa>)\<close>
+  have "\<kappa> < \<kappa>\<^sup>+" "Card(\<kappa>\<^sup>+)"
+    using csucc_basic by simp_all
+  moreover
+  assume "d \<lesssim> \<kappa>"
+  ultimately
+  have "d \<lesssim> \<kappa>\<^sup>+"
+    using le_imp_lepoll leI lepoll_trans by simp
+  moreover
+  from \<open>d \<lesssim> \<kappa>\<close> \<open>Ord(\<kappa>)\<close>
+  have "\<kappa>\<^sup>+ \<lesssim> \<kappa>" if "d \<approx> \<kappa>\<^sup>+"
+    using eqpoll_sym[OF that] eq_lepoll_trans[OF _ \<open>d\<lesssim>\<kappa>\<close>] by simp
+  moreover from calculation \<open>Card(_)\<close>
+  have "\<not> d \<approx> \<kappa>\<^sup>+"
+    using lesspoll_irrefl lesspoll_trans1 lt_Card_imp_lesspoll[OF _ \<open>\<kappa> <_\<close>]
+    by auto
+  ultimately
+  show "d \<prec> \<kappa>\<^sup>+"
+    unfolding lesspoll_def by simp
+qed
+
+abbreviation
+  Infinite :: "i\<Rightarrow>o" where
+  "Infinite(X) \<equiv> \<not> Finite(X)"
+
+lemma Infinite_not_empty: "Infinite(X) \<Longrightarrow> X \<noteq> 0"
+  using empty_lepollI by auto
+
+lemma Infinite_imp_nats_lepoll:
+  assumes "Infinite(X)" "n \<in> \<omega>"
+  shows "n \<lesssim> X"
+  using \<open>n \<in> \<omega>\<close>
+proof (induct)
+  case 0
+  then
+  show ?case using empty_lepollI by simp
+next
+  case (succ x)
+  show ?case
+  proof -
+    from \<open>Infinite(X)\<close> and \<open>x \<in> \<omega>\<close>
+    have "\<not> (x \<approx> X)"
+      using eqpoll_sym unfolding Finite_def by auto
+    with \<open>x \<lesssim> X\<close>
+    obtain f where "f \<in> inj(x,X)" "f \<notin> surj(x,X)"
+      unfolding bij_def eqpoll_def by auto
+    moreover from this
+    obtain b where "b \<in> X" "\<forall>a\<in>x. f`a \<noteq> b"
+      using inj_is_fun unfolding surj_def by auto
+    ultimately
+    have "f \<in> inj(x,X-{b})"
+      unfolding inj_def by (auto intro:Pi_type)
+    then
+    have "cons(\<langle>x, b\<rangle>, f) \<in> inj(succ(x), cons(b, X - {b}))"
+      using inj_extend[of f x "X-{b}" x b] unfolding succ_def
+      by (auto dest:mem_irrefl)
+    moreover from \<open>b\<in>X\<close>
+    have "cons(b, X - {b}) = X" by auto
+    ultimately
+    show "succ(x) \<lesssim> X" by auto
+  qed
+qed
+
+lemma zero_lesspoll: assumes "0<\<kappa>" shows "0 \<prec> \<kappa>"
+  using assms eqpoll_0_iff[THEN iffD1, of \<kappa>] eqpoll_sym
+  unfolding lesspoll_def lepoll_def
+  by (auto simp add:inj_def)
+
+lemma lepoll_nat_imp_Infinite: "\<omega> \<lesssim> X \<Longrightarrow> Infinite(X)"
+proof (rule ccontr, simp)
+  assume "\<omega> \<lesssim> X" "Finite(X)"
+  moreover from this
+  obtain n where "X \<approx> n" "n \<in> \<omega>"
+    unfolding Finite_def by auto
+  moreover from calculation
+  have "\<omega> \<lesssim> n"
+    using lepoll_eq_trans by simp
+  ultimately
+  show "False"
+    using lepoll_nat_imp_Finite nat_not_Finite by simp
+qed
+
+lemma InfCard_imp_Infinite: "InfCard(\<kappa>) \<Longrightarrow> Infinite(\<kappa>)"
+  using le_imp_lepoll[THEN lepoll_nat_imp_Infinite, of \<kappa>]
+  unfolding InfCard_def by simp
+
+lemma lt_surj_empty_imp_Card:
+  assumes "Ord(\<kappa>)" "\<And>\<alpha>. \<alpha> < \<kappa> \<Longrightarrow> surj(\<alpha>,\<kappa>) = 0"
+  shows "Card(\<kappa>)"
+proof -
+  {
+    assume "|\<kappa>| < \<kappa>"
+    with assms
+    have "False"
+      using LeastI[of "\<lambda>i. i \<approx> \<kappa>" \<kappa>, OF eqpoll_refl]
+        Least_le[of "\<lambda>i. i \<approx> \<kappa>" "|\<kappa>|", OF Ord_cardinal_eqpoll]
+      unfolding Card_def cardinal_def eqpoll_def bij_def
+      by simp
+  }
+  with assms
+  show ?thesis
+    using Ord_cardinal_le[of \<kappa>] not_lt_imp_le[of "|\<kappa>|" \<kappa>] le_anti_sym
+    unfolding Card_def by auto
+qed
+
+
+subsection\<open>Morphisms of binary relations\<close>
+
+text\<open>The main case of interest is in the case of partial orders.\<close>
+
+lemma mono_map_mono:
+  assumes
+    "f \<in> mono_map(A,r,B,s)" "B \<subseteq> C"
+  shows
+    "f \<in> mono_map(A,r,C,s)"
+  unfolding mono_map_def
+proof (intro CollectI ballI impI)
+  from \<open>f \<in> mono_map(A,_,B,_)\<close>
+  have "f: A \<rightarrow> B"
+    using mono_map_is_fun by simp
+  with \<open>B\<subseteq>C\<close>
+  show "f: A \<rightarrow> C"
+    using fun_weaken_type by simp
+  fix x y
+  assume "x\<in>A" "y\<in>A" "\<langle>x,y\<rangle> \<in> r"
+  moreover from this and \<open>f: A \<rightarrow> B\<close>
+  have "f`x \<in> B" "f`y \<in> B"
+    using apply_type by simp_all
+  moreover
+  note \<open>f \<in> mono_map(_,r,_,s)\<close>
+  ultimately
+  show "\<langle>f ` x, f ` y\<rangle> \<in> s"
+    unfolding mono_map_def by blast
+qed
+
+lemma ordertype_zero_imp_zero: "ordertype(A,r) = 0 \<Longrightarrow> A = 0"
+  using ordermap_type[of A r]
+  by (cases "A=0") auto
+
+lemma mono_map_increasing:
+  "j\<in>mono_map(A,r,B,s) \<Longrightarrow> a\<in>A \<Longrightarrow> c\<in>A \<Longrightarrow> \<langle>a,c\<rangle>\<in>r \<Longrightarrow> \<langle>j`a,j`c\<rangle>\<in>s"
+  unfolding mono_map_def by simp
+
+lemma linear_mono_map_reflects:
+  assumes
+    "linear(\<alpha>,r)" "trans[\<beta>](s)" "irrefl(\<beta>,s)" "f\<in>mono_map(\<alpha>,r,\<beta>,s)"
+    "x\<in>\<alpha>" "y\<in>\<alpha>" "\<langle>f`x,f`y\<rangle>\<in>s"
+  shows
+    "\<langle>x,y\<rangle>\<in>r"
+proof -
+  from \<open>f\<in>mono_map(_,_,_,_)\<close>
+  have preserves:"x\<in>\<alpha> \<Longrightarrow> y\<in>\<alpha> \<Longrightarrow> \<langle>x,y\<rangle>\<in>r \<Longrightarrow> \<langle>f`x,f`y\<rangle>\<in>s" for x y
+    unfolding mono_map_def by blast
+  {
+    assume "\<langle>x, y\<rangle> \<notin> r" "x\<in>\<alpha>" "y\<in>\<alpha>"
+    moreover
+    note \<open>\<langle>f`x,f`y\<rangle>\<in>s\<close> and \<open>linear(\<alpha>,r)\<close>
+    moreover from calculation
+    have "y = x \<or> \<langle>y,x\<rangle>\<in>r"
+      unfolding linear_def by blast
+    moreover
+    note preserves [of y x]
+    ultimately
+    have "y = x \<or> \<langle>f`y, f`x\<rangle>\<in> s" by blast
+    moreover from \<open>f\<in>mono_map(_,_,\<beta>,_)\<close> \<open>x\<in>\<alpha>\<close> \<open>y\<in>\<alpha>\<close>
+    have "f`x\<in>\<beta>" "f`y\<in>\<beta>"
+      using apply_type[OF mono_map_is_fun] by simp_all
+    moreover
+    note \<open>\<langle>f`x,f`y\<rangle>\<in>s\<close>  \<open>trans[\<beta>](s)\<close> \<open>irrefl(\<beta>,s)\<close>
+    ultimately
+    have "False"
+      using trans_onD[of \<beta> s "f`x" "f`y" "f`x"] irreflE by blast
+  }
+  with assms
+  show "\<langle>x,y\<rangle>\<in>r" by blast
+qed
+
+lemma irrefl_Memrel: "irrefl(x, Memrel(x))"
+  unfolding irrefl_def using mem_irrefl by auto
+
+lemmas Memrel_mono_map_reflects = linear_mono_map_reflects
+  [OF well_ord_is_linear[OF well_ord_Memrel] well_ord_is_trans_on[OF well_ord_Memrel]
+    irrefl_Memrel]
+
+\<comment> \<open>Same proof as Paulson's @{thm mono_map_is_inj}\<close>
+lemma mono_map_is_inj':
+  "\<lbrakk> linear(A,r);  irrefl(B,s);  f \<in> mono_map(A,r,B,s) \<rbrakk> \<Longrightarrow> f \<in> inj(A,B)"
+  unfolding irrefl_def mono_map_def inj_def using linearE
+  by (clarify, rename_tac x w)
+    (erule_tac x=w and y=x in linearE, assumption+, (force intro: apply_type)+)
+
+lemma mono_map_imp_ord_iso_image:
+  assumes
+    "linear(\<alpha>,r)" "trans[\<beta>](s)"  "irrefl(\<beta>,s)" "f\<in>mono_map(\<alpha>,r,\<beta>,s)"
+  shows
+    "f \<in> ord_iso(\<alpha>,r,f``\<alpha>,s)"
+  unfolding ord_iso_def
+proof (intro CollectI ballI iffI)
+  \<comment> \<open>Enough to show it's bijective and preserves both ways\<close>
+  from assms
+  have "f \<in> inj(\<alpha>,\<beta>)"
+    using mono_map_is_inj' by blast
+  moreover from \<open>f \<in> mono_map(_,_,_,_)\<close>
+  have "f \<in> surj(\<alpha>, f``\<alpha>)"
+    unfolding mono_map_def using surj_image by auto
+  ultimately
+  show "f \<in> bij(\<alpha>, f``\<alpha>)"
+    unfolding bij_def using inj_is_fun inj_to_Image by simp
+  from \<open>f\<in>mono_map(_,_,_,_)\<close>
+  show "x\<in>\<alpha> \<Longrightarrow> y\<in>\<alpha> \<Longrightarrow> \<langle>x,y\<rangle>\<in>r \<Longrightarrow> \<langle>f`x,f`y\<rangle>\<in>s" for x y
+    unfolding mono_map_def by blast
+  with assms
+  show "\<langle>f`x,f`y\<rangle>\<in>s \<Longrightarrow> x\<in>\<alpha> \<Longrightarrow> y\<in>\<alpha> \<Longrightarrow> \<langle>x,y\<rangle>\<in>r" for x y
+    using linear_mono_map_reflects
+    by blast
+qed
+
+text\<open>We introduce the following notation for strictly increasing maps
+between ordinals.\<close>
+
+abbreviation
+  mono_map_Memrel :: "[i,i] \<Rightarrow> i" (infixr \<open>\<rightarrow>\<^sub><\<close> 60) where
+  "\<alpha> \<rightarrow>\<^sub>< \<beta> \<equiv> mono_map(\<alpha>,Memrel(\<alpha>),\<beta>,Memrel(\<beta>))"
+
+lemma mono_map_imp_ord_iso_Memrel:
+  assumes
+    "Ord(\<alpha>)" "Ord(\<beta>)" "f:\<alpha> \<rightarrow>\<^sub>< \<beta>"
+  shows
+    "f \<in> ord_iso(\<alpha>,Memrel(\<alpha>),f``\<alpha>,Memrel(\<beta>))"
+  using assms mono_map_imp_ord_iso_image[OF well_ord_is_linear[OF well_ord_Memrel]
+      well_ord_is_trans_on[OF well_ord_Memrel] irrefl_Memrel] by blast
+
+lemma mono_map_ordertype_image':
+  assumes
+    "X\<subseteq>\<alpha>" "Ord(\<alpha>)" "Ord(\<beta>)" "f \<in> mono_map(X,Memrel(\<alpha>),\<beta>,Memrel(\<beta>))"
+  shows
+    "ordertype(f``X,Memrel(\<beta>)) = ordertype(X,Memrel(\<alpha>))"
+  using assms mono_map_is_fun[of f X _ \<beta>]  ordertype_eq
+    mono_map_imp_ord_iso_image[OF well_ord_is_linear[OF well_ord_Memrel, THEN linear_subset]
+      well_ord_is_trans_on[OF well_ord_Memrel] irrefl_Memrel, of \<alpha> X \<beta> f]
+    well_ord_subset[OF well_ord_Memrel]  Image_sub_codomain[of f X \<beta> X] by auto
+
+lemma mono_map_ordertype_image:
+  assumes
+    "Ord(\<alpha>)" "Ord(\<beta>)" "f:\<alpha> \<rightarrow>\<^sub>< \<beta>"
+  shows
+    "ordertype(f``\<alpha>,Memrel(\<beta>)) = \<alpha>"
+  using assms mono_map_is_fun ordertype_Memrel ordertype_eq[of f \<alpha> "Memrel(\<alpha>)"]
+    mono_map_imp_ord_iso_Memrel well_ord_subset[OF well_ord_Memrel] Image_sub_codomain[of _ \<alpha>]
+  by auto
+
+lemma apply_in_image: "f:A\<rightarrow>B \<Longrightarrow> a\<in>A \<Longrightarrow> f`a \<in> f``A"
+  using range_eq_image apply_rangeI[of f]  by simp
+
+lemma Image_subset_Ord_imp_lt:
+  assumes
+    "Ord(\<alpha>)" "h``A \<subseteq> \<alpha>" "x\<in>domain(h)" "x\<in>A" "function(h)"
+  shows
+    "h`x < \<alpha>"
+  using assms
+  unfolding domain_def using imageI ltI function_apply_equality by auto
+
+lemma ordermap_le_arg:
+  assumes
+    "X\<subseteq>\<beta>" "x\<in>X" "Ord(\<beta>)"
+  shows
+    "x\<in>X \<Longrightarrow> ordermap(X,Memrel(\<beta>))`x\<le>x"
+proof (induct rule:Ord_induct[OF subsetD, OF assms])
+  case (1 x)
+  have "wf[X](Memrel(\<beta>))"
+    using wf_imp_wf_on[OF wf_Memrel] .
+  with 1
+  have "ordermap(X,Memrel(\<beta>))`x = {ordermap(X,Memrel(\<beta>))`y . y\<in>{y\<in>X . y\<in>x \<and> y\<in>\<beta>}}"
+    using ordermap_unfold Ord_trans[of _ x \<beta>] by auto
+  also from assms
+  have "... = {ordermap(X,Memrel(\<beta>))`y . y\<in>{y\<in>X . y\<in>x}}"
+    using Ord_trans[of _ x \<beta>] Ord_in_Ord by blast
+  finally
+  have ordm:"ordermap(X,Memrel(\<beta>))`x = {ordermap(X,Memrel(\<beta>))`y . y\<in>{y\<in>X . y\<in>x}}" .
+  from 1
+  have "y\<in>x \<Longrightarrow> y\<in>X \<Longrightarrow> ordermap(X,Memrel(\<beta>))`y \<le> y" for y by simp
+  with \<open>x\<in>\<beta>\<close> and \<open>Ord(\<beta>)\<close>
+  have "y\<in>x \<Longrightarrow> y\<in>X \<Longrightarrow> ordermap(X,Memrel(\<beta>))`y \<in> x" for y
+    using ltI[OF _ Ord_in_Ord[of \<beta> x]] lt_trans1 ltD by blast
+  with ordm
+  have "ordermap(X,Memrel(\<beta>))`x \<subseteq> x" by auto
+  with \<open>x\<in>X\<close> assms
+  show ?case
+    using subset_imp_le Ord_in_Ord[of \<beta> x] Ord_ordermap
+      well_ord_subset[OF well_ord_Memrel, of \<beta>] by force
+qed
+
+lemma subset_imp_ordertype_le:
+  assumes
+    "X\<subseteq>\<beta>" "Ord(\<beta>)"
+  shows
+    "ordertype(X,Memrel(\<beta>))\<le>\<beta>"
+proof -
+  {
+    fix x
+    assume "x\<in>X"
+    with assms
+    have "ordermap(X,Memrel(\<beta>))`x \<le> x"
+      using ordermap_le_arg by simp
+    with \<open>x\<in>X\<close> and assms
+    have "ordermap(X,Memrel(\<beta>))`x \<in> \<beta>" (is "?y \<in> _")
+      using ltD[of ?y "succ(x)"] Ord_trans[of  ?y x \<beta>] by auto
+  }
+  then
+  have "ordertype(X, Memrel(\<beta>)) \<subseteq> \<beta>"
+    using ordertype_unfold[of X] by auto
+  with assms
+  show ?thesis
+    using subset_imp_le Ord_ordertype[OF well_ord_subset, OF well_ord_Memrel] by simp
+qed
+
+lemma mono_map_imp_le:
+  assumes
+    "f\<in>mono_map(\<alpha>, Memrel(\<alpha>),\<beta>, Memrel(\<beta>))" "Ord(\<alpha>)" "Ord(\<beta>)"
+  shows
+    "\<alpha>\<le>\<beta>"
+proof -
+  from assms
+  have "f \<in> \<langle>\<alpha>, Memrel(\<alpha>)\<rangle> \<cong> \<langle>f``\<alpha>, Memrel(\<beta>)\<rangle>"
+    using mono_map_imp_ord_iso_Memrel by simp
+  then
+  have "converse(f) \<in> \<langle>f``\<alpha>, Memrel(\<beta>)\<rangle> \<cong> \<langle>\<alpha>, Memrel(\<alpha>)\<rangle>"
+    using ord_iso_sym by simp
+  with \<open>Ord(\<alpha>)\<close>
+  have "\<alpha> = ordertype(f``\<alpha>,Memrel(\<beta>))"
+    using ordertype_eq well_ord_Memrel ordertype_Memrel by auto
+  also from assms
+  have "ordertype(f``\<alpha>,Memrel(\<beta>)) \<le> \<beta>"
+    using subset_imp_ordertype_le mono_map_is_fun[of f] Image_sub_codomain[of f] by force
+  finally
+  show ?thesis .
+qed
+
+\<comment> \<open>\<^term>\<open>Ord(A) \<Longrightarrow> f \<in> mono_map(A, Memrel(A), B, Memrel(Aa)) \<Longrightarrow> f \<in> inj(A, B)\<close>\<close> 
+lemmas Memrel_mono_map_is_inj = mono_map_is_inj
+  [OF well_ord_is_linear[OF well_ord_Memrel]
+    wf_imp_wf_on[OF wf_Memrel]]
+
+lemma mono_mapI:
+  assumes "f: A\<rightarrow>B" "\<And>x y. x\<in>A \<Longrightarrow> y\<in>A \<Longrightarrow> \<langle>x,y\<rangle>\<in>r \<Longrightarrow> \<langle>f`x,f`y\<rangle>\<in>s"
+  shows   "f \<in> mono_map(A,r,B,s)"
+  unfolding mono_map_def using assms by simp
+
+lemmas mono_mapD = mono_map_is_fun mono_map_increasing
+
+bundle mono_map_rules =  mono_mapI[intro!] mono_map_is_fun[dest] mono_mapD[dest]
+
+lemma nats_le_InfCard:
+  assumes "n \<in> \<omega>" "InfCard(\<kappa>)"
+  shows "n \<le> \<kappa>"
+  using assms Ord_is_Transset
+    le_trans[of n \<omega> \<kappa>, OF le_subset_iff[THEN iffD2]]
+  unfolding InfCard_def Transset_def by simp
+
+lemma nat_into_InfCard:
+  assumes "n \<in> \<omega>" "InfCard(\<kappa>)"
+  shows "n \<in> \<kappa>"
+  using assms  le_imp_subset[of \<omega> \<kappa>]
+  unfolding InfCard_def by auto
+
+
+subsection\<open>Alephs are infinite cardinals\<close>
+
+lemma Aleph_zero_eq_nat: "\<aleph>\<^bsub>0\<^esub> = \<omega>"
+  unfolding Aleph_def by simp
+
+lemma InfCard_Aleph:
+  notes Aleph_zero_eq_nat[simp]
+  assumes "Ord(\<alpha>)"
+  shows "InfCard(\<aleph>\<^bsub>\<alpha>\<^esub>)"
+proof -
+  have "\<not> (\<aleph>\<^bsub>\<alpha>\<^esub> \<in> \<omega>)"
+  proof (cases "\<alpha>=0")
+    case True
+    then show ?thesis using mem_irrefl by auto
+  next
+    case False
+    with \<open>Ord(\<alpha>)\<close>
+    have "\<omega> \<in> \<aleph>\<^bsub>\<alpha>\<^esub>" using Ord_0_lt[of \<alpha>] ltD  by (auto dest:Aleph_increasing)
+    then show ?thesis using foundation by blast
+  qed
+  with \<open>Ord(\<alpha>)\<close>
+  have "\<not> (|\<aleph>\<^bsub>\<alpha>\<^esub>| \<in> \<omega>)"
+    using Card_cardinal_eq by auto
+  then
+  have "\<not> Finite(\<aleph>\<^bsub>\<alpha>\<^esub>)" by auto
+  with \<open>Ord(\<alpha>)\<close>
+  show ?thesis
+    using Inf_Card_is_InfCard by simp
+qed
+
+lemmas Limit_Aleph = InfCard_Aleph[THEN InfCard_is_Limit]
+
+lemmas Aleph_cont = Normal_imp_cont[OF Normal_Aleph]
+lemmas Aleph_sup = Normal_Union[OF _ _ Normal_Aleph]
+
+bundle Ord_dests = Limit_is_Ord[dest] Card_is_Ord[dest]
+bundle Aleph_dests = Aleph_cont[dest] Aleph_sup[dest]
+bundle Aleph_intros = Aleph_increasing[intro!]
+bundle Aleph_mem_dests = Aleph_increasing[OF ltI, THEN ltD, dest]
+
+
+end
\ No newline at end of file
diff --git a/thys/Delta_System_Lemma/document/header-delta-system.tex b/thys/Delta_System_Lemma/document/header-delta-system.tex
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/document/header-delta-system.tex
@@ -0,0 +1,295 @@
+\usepackage[utf8]{inputenc}
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{bbm}  % Para el \bb{1}
+\usepackage{multidef}
+\usepackage{verbatim}
+\usepackage{stmaryrd} %% para \llbracket
+% \usepackage{hyperref}
+\usepackage{xcolor}
+\usepackage{framed}
+
+%%
+%% \usepackage[bottom=2cm, top=2cm, left=2cm, right=2cm]{geometry}
+%% \usepackage{titling}
+%% \setlength{\droptitle}{-10ex} 
+%%
+\renewcommand{\o}{\vee}
+\renewcommand{\O}{\bigvee}
+\newcommand{\y}{\wedge}
+\newcommand{\Y}{\bigwedge}
+\newcommand{\limp}{\longrightarrow}
+\newcommand{\lsii}{\longleftrightarrow}
+%%
+%\newcommand{\DeclareMathOperator}[2]{\newcommand{#1}{\mathop{\mathrm{#2}}}}
+
+\DeclareMathOperator{\cf}{cf}
+\DeclareMathOperator{\dom}{domain}
+\DeclareMathOperator{\im}{img}
+\DeclareMathOperator{\Fn}{Fn}
+\DeclareMathOperator{\rk}{rk}
+\DeclareMathOperator{\mos}{mos}
+\DeclareMathOperator{\trcl}{trcl}
+\DeclareMathOperator{\Con}{Con}
+\DeclareMathOperator{\Club}{Club}
+
+
+\newcommand{\modelo}[1]{\mathbf{#1}}
+\newcommand{\axiomas}[1]{\mathit{#1}}
+\newcommand{\clase}[1]{\mathsf{#1}}
+\newcommand{\poset}[1]{\mathbb{#1}}
+\newcommand{\operador}[1]{\mathbf{#1}}
+
+%% \newcommand{\Lim}{\clase{Lim}}
+%% \newcommand{\Reg}{\clase{Reg}}
+%% \newcommand{\Card}{\clase{Card}}
+%% \newcommand{\On}{\clase{On}}
+%% \newcommand{\WF}{\clase{WF}}
+%% \newcommand{\HF}{\clase{HF}}
+%% \newcommand{\HC}{\clase{HC}}
+%%
+%% El siguiente comando reemplaza todos los anteriores:
+%%
+\multidef{\clase{#1}}{Card,HC,HF,Lim,On->Ord,Reg,WF,Ord}
+\newcommand{\ON}{\On}
+
+%% En lugar de usar todo el paquete bbm:
+\DeclareMathAlphabet{\mathbbm}{U}{bbm}{m}{n} 
+\newcommand{\1}{\mathbbm{1}}
+\newcommand{\PP}{\mathbbm{P}}
+
+%%
+%% \newcommand{\calD}{\mathcal{D}}
+%% \newcommand{\calS}{\mathcal{S}}
+%% \newcommand{\calU}{\mathcal{U}}
+%% \newcommand{\calB}{\mathcal{B}}
+%% \newcommand{\calL}{\mathcal{L}}
+%% \newcommand{\calF}{\mathcal{F}}
+%% \newcommand{\calT}{\mathcal{T}}
+%% \newcommand{\calW}{\mathcal{W}}
+%% \newcommand{\calA}{\mathcal{A}}
+%%
+%% El siguiente comando reemplaza todos los anteriores:
+%%
+\multidef[prefix=cal]{\mathcal{#1}}{A-Z}
+%%
+%% \newcommand{\A}{\modelo{A}}
+%% \newcommand{\BB}{\modelo{B}}
+%% \newcommand{\ZZ}{\modelo{Z}}
+%% \newcommand{\PP}{\modelo{P}}
+%% \newcommand{\QQ}{\modelo{Q}}
+%% \newcommand{\RR}{\modelo{R}}
+%%
+%% El siguiente comando reemplaza todos los anteriores:
+%%
+\multidef{\modelo{#1}}{A,BB->B,CC->C,NN->N,QQ->Q,RR->R,ZZ->Z}
+
+\multidef[prefix=p]{\mathbb{#1}}{A-Z}
+%% \newcommand{\B}{\modelo{B}}
+%% \newcommand{\C}{\modelo{C}}
+%% \newcommand{\F}{\modelo{F}}
+%% \newcommand{\D}{\modelo{D}}
+
+\newcommand{\Th}{\mb{Th}}
+\newcommand{\Mod}{\mb{Mod}}
+
+\newcommand{\Se}{\operador{S^\prec}}
+\newcommand{\Pu}{\operador{P_u}}
+\renewcommand{\Pr}{\operador{P_R}}
+\renewcommand{\H}{\operador{H}}
+\renewcommand{\S}{\operador{S}}
+\newcommand{\I}{\operador{I}}
+\newcommand{\E}{\operador{E}}
+
+\newcommand{\se}{\preccurlyeq}
+\newcommand{\ee}{\succ}
+\newcommand{\id}{\approx}
+\newcommand{\subm}{\subseteq}
+\newcommand{\ext}{\supseteq}
+\newcommand{\iso}{\cong}
+%%
+\renewcommand{\emptyset}{\varnothing}
+\newcommand{\rel}{\mathcal{R}}
+\newcommand{\Pow}{\mathop{\mathcal{P}}}
+\renewcommand{\P}{\Pow}
+\newcommand{\BP}{\mathrm{BP}}
+\newcommand{\func}{\rightarrow}
+\newcommand{\ord}{\mathrm{Ord}}
+\newcommand{\R}{\mathbb{R}}
+\newcommand{\N}{\mathbb{N}}
+\newcommand{\Z}{\mathbb{Z}}
+\renewcommand{\I}{\mathbb{I}}
+\newcommand{\Q}{\mathbb{Q}}
+\newcommand{\B}{\mathbf{B}}
+\newcommand{\lb}{\langle}
+\newcommand{\rb}{\rangle}
+\newcommand{\impl}{\rightarrow}
+\newcommand{\ent}{\Rightarrow}
+\newcommand{\tne}{\Leftarrow}
+\newcommand{\sii}{\Leftrightarrow}
+\renewcommand{\phi}{\varphi}
+\newcommand{\phis}{{\varphi^*}}
+\renewcommand{\th}{\theta}
+\newcommand{\Lda}{\Lambda}
+\newcommand{\La}{\Lambda}
+\newcommand{\lda}{\lambda}
+\newcommand{\ka}{\kappa}
+\newcommand{\del}{\delta}
+\newcommand{\de}{\delta}
+\newcommand{\ze}{\zeta}
+%\newcommand{\ }{\ }
+\newcommand{\la}{\lambda}
+\newcommand{\al}{\alpha}
+\newcommand{\be}{\beta}
+\newcommand{\ga}{\gamma}
+\newcommand{\Ga}{\Gamma}
+\newcommand{\ep}{\varepsilon}
+\newcommand{\De}{\Delta}
+\newcommand{\defi}{\mathrel{\mathop:}=}
+\newcommand{\forces}{\Vdash}
+%\newcommand{\ap}{\mathbin{\wideparen{\ }}}
+\newcommand{\Tree}{{\mathrm{Tr}_\N}}
+\newcommand{\PTree}{{\mathrm{PTr}_\N}}
+\newcommand{\NWO}{\mathit{NWO}}
+\newcommand{\Suc}{{\N^{<\N}}}%
+\newcommand{\init}{\mathsf{i}}
+\newcommand{\ap}{\mathord{^\smallfrown}}
+\newcommand{\Cantor}{\mathcal{C}}
+%\newcommand{\C}{\Cantor}
+\newcommand{\Baire}{\mathcal{N}}
+\newcommand{\sig}{\ensuremath{\sigma}}
+\newcommand{\fsig}{\ensuremath{F_\sigma}}
+\newcommand{\gdel}{\ensuremath{G_\delta}}
+\newcommand{\Sig}{\ensuremath{\boldsymbol{\Sigma}}}
+\newcommand{\bPi}{\ensuremath{\boldsymbol{\Pi}}}
+\newcommand{\Del}{\ensuremath{\boldsymbol\Delta}}
+%\renewcommand{\F}{\operador{F}}
+\newcommand{\ths}{{\theta^*}}
+\newcommand{\om}{\ensuremath{\omega}}
+%\renewcommand{\c}{\complement}
+\newcommand{\comp}{\mathsf{c}}
+\newcommand{\co}[1]{\left(#1\right)^\comp}
+\newcommand{\len}[1]{\left|#1\right|}
+\DeclareMathOperator{\tlim}{\overline{\mathrm{TLim}}}
+\newcommand{\card}[1]{{\left|#1\right|}}
+\newcommand{\bigcard}[1]{{\bigl|#1\bigr|}}
+%
+% Cardinality
+%
+\newcommand{\lec}{\leqslant_c}
+\newcommand{\gec}{\geqslant_c}
+\newcommand{\lc}{<_c}
+\newcommand{\gc}{>_c}
+\newcommand{\eqc}{=_c}
+\newcommand{\biy}{\approx}
+\newcommand*{\ale}[1]{\aleph_{#1}}
+%
+\newcommand{\Zerm}{\axiomas{Z}}
+\newcommand{\ZC}{\axiomas{ZC}}
+\newcommand{\AC}{\axiomas{AC}}
+\newcommand{\DC}{\axiomas{DC}}
+\newcommand{\MA}{\axiomas{MA}}
+\newcommand{\CH}{\axiomas{CH}}
+\newcommand{\ZFC}{\axiomas{ZFC}}
+\newcommand{\ZF}{\axiomas{ZF}}
+\newcommand{\Inf}{\axiomas{Inf}}
+%
+% Cardinal characteristics
+%
+\newcommand{\cont}{\mathfrak{c}}
+\newcommand{\spl}{\mathfrak{s}}
+\newcommand{\bound}{\mathfrak{b}}
+\newcommand{\mad}{\mathfrak{a}}
+\newcommand{\tower}{\mathfrak{t}}
+%
+\renewcommand{\hom}[2]{{}^{#1}\hskip-0.116ex{#2}}
+\newcommand{\pred}[1][{}]{\mathop{\mathrm{pred}_{#1}}}
+%% Postfix operator with supressable space:
+%% \newcommand*{\iseg}{\relax\ifnum\lastnodetype>0 \mskip\medmuskip\fi{\downarrow}} %
+\newcommand*{\iseg}{{\downarrow}}
+\newcommand{\rr}{\mathrel{R}}
+\newcommand{\restr}{\upharpoonright}
+%\newcommand{\type}{\mathtt{}}
+\newcommand{\app}{\mathop{\mathrm{Aprox}}}
+\newcommand{\hess}{\triangleleft}
+\newcommand{\bx}{\bar{x}}
+\newcommand{\by}{\bar{y}}
+\newcommand{\bz}{\bar{z}}
+\newcommand{\union}{\mathop{\textstyle\bigcup}}
+\newcommand{\sm}{\setminus}
+\newcommand{\sbq}{\subseteq}
+\newcommand{\nsbq}{\subseteq}
+\newcommand{\mty}{\emptyset}
+\newcommand{\dimg}{\text{\textup{``}}} % direct image
+\newcommand{\quine}[1]{\ulcorner{\!#1\!}\urcorner}
+%\newcommand{\ntrm}[1]{\textsl{\textbf{#1}}}
+\newcommand{\Null}{\calN\!\mathit{ull}}
+\DeclareMathOperator{\club}{Club}
+\DeclareMathOperator{\otp}{otp}
+\DeclareMathOperator{\val}{\mathit{val}}
+\DeclareMathOperator{\chk}{\mathit{check}}
+\DeclareMathOperator{\edrel}{\mathit{edrel}}
+\DeclareMathOperator{\eclose}{\mathit{eclose}}
+\DeclareMathOperator{\Memrel}{\mathit{Memrel}}
+\renewcommand{\PP}{\mathbb{P}}
+\renewcommand{\app}{\mathrm{App}}
+\newcommand{\formula}{\isatt{formula}}
+\newcommand{\tyi}{\isatt{i}}
+\newcommand{\tyo}{\isatt{o}}
+\newcommand{\forceisa}{\mathop{\mathtt{forces}}}
+\newcommand{\equ}{\mathbf{e}}
+\newcommand{\bel}{\mathbf{b}}
+\newcommand{\atr}{\mathit{atr}}
+\newcommand{\concat}{\mathbin{@}}
+\newcommand{\dB}[1]{\mathbf{#1}}
+\newcommand{\ed}{\mathrel{\isatt{ed}}}
+\newcommand{\frecR}{\mathrel{\isatt{frecR}}}
+\newcommand{\forceseq}{\mathop{\isatt{forces{\isacharunderscore}eq}}}
+\newcommand{\forcesmem}{\mathop{\isatt{forces{\isacharunderscore}mem}}}
+\newcommand{\forcesat}{\mathop{\isatt{forces{\isacharunderscore}at}}}
+\newcommand{\pleq}{\preceq}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%
+% Variant aleph, beth, etc
+% From http://tex.stackexchange.com/q/170476/69595
+\makeatletter
+\@ifpackageloaded{txfonts}\@tempswafalse\@tempswatrue
+\if@tempswa
+  \DeclareFontFamily{U}{txsymbols}{}
+  \DeclareFontFamily{U}{txAMSb}{}
+  \DeclareSymbolFont{txsymbols}{OMS}{txsy}{m}{n}
+  \SetSymbolFont{txsymbols}{bold}{OMS}{txsy}{bx}{n}
+  \DeclareFontSubstitution{OMS}{txsy}{m}{n}
+  \DeclareSymbolFont{txAMSb}{U}{txsyb}{m}{n}
+  \SetSymbolFont{txAMSb}{bold}{U}{txsyb}{bx}{n}
+  \DeclareFontSubstitution{U}{txsyb}{m}{n}
+  \DeclareMathSymbol{\aleph}{\mathord}{txsymbols}{64}
+  \DeclareMathSymbol{\beth}{\mathord}{txAMSb}{105}
+  \DeclareMathSymbol{\gimel}{\mathord}{txAMSb}{106}
+  \DeclareMathSymbol{\daleth}{\mathord}{txAMSb}{107}
+\fi
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%
+%% Theorem Environments
+%%
+% \newtheorem{theorem}{Theorem}
+% \newtheorem{lemma}[theorem]{Lemma}
+% \newtheorem{prop}[theorem]{Proposition}
+% \newtheorem{corollary}[theorem]{Corollary}
+% \newtheorem{claim}{Claim}
+% \newtheorem*{claim*}{Claim}
+% \theoremstyle{definition}
+% \newtheorem{definition}[theorem]{Definition}
+% \newtheorem{remark}[theorem]{Remark}
+% \newtheorem{example}[theorem]{Example}
+% \theoremstyle{remark}
+% \newtheorem*{remark*}{Remark}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%% \newenvironment{inducc}{\begin{list}{}{\itemindent=2.5em \labelwidth=4em}}{\end{list}}
+%% \newcommand{\caso}[1]{\item[\fbox{#1}]}
+\newenvironment{proofofclaim}{\begin{proof}[Proof of Claim]}{\end{proof}}
diff --git a/thys/Delta_System_Lemma/document/multidef.sty b/thys/Delta_System_Lemma/document/multidef.sty
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/document/multidef.sty
@@ -0,0 +1,133 @@
+%%
+%% This is file `multidef.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% multidef.dtx  (with options: `package')
+%% 
+%% (c) 2016/03/14 Nicolas Markey <multidef at markey dot fr>
+%% 
+%% This work may  be distributed and/or modified under  the conditions of
+%% the LaTeX Project  Public License, either version 1.3  of this license
+%% or (at  your option)  any later version.   The latest version  of this
+%% license is in
+%% 
+%%   http://www.latex-project.org/lppl.txt
+%% 
+%% and version 1.3 or later is part of all distributions of LaTeX version
+%% 2005/12/01 or later.
+%% 
+%% This work has the LPPL maintenance status `maintained'.
+%% The Current Maintainer of this work is Nicolas Markey.
+%% 
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+%%
+\RequirePackage{xkeyval}
+\define@boolkeys{mdef}{noerr,nowarn}[true]
+\DeclareOptionX{noerr}[true]{\setkeys{mdef}{noerr=#1}}
+\DeclareOptionX{nowarn}[true]{\setkeys{mdef}{nowarn=#1}}
+\ExecuteOptionsX{noerr=false,nowarn=false}
+\ProcessOptionsX
+\ifKV@mdef@noerr
+\presetkeys{mdef}{noerr=true}{}
+\else
+\presetkeys{mdef}{noerr=false}{}
+\fi
+\ifKV@mdef@nowarn
+\presetkeys{mdef}{nowarn=true}{}
+\else
+\presetkeys{mdef}{nowarn=false}{}
+\fi
+\define@key{mdef}{prefix}{\def\@mdprefix{#1}}
+\define@key{mdef}{p}{\def\@mdprefix{#1}}
+\define@key{mdef}{suffix}{\def\@mdsuffix{#1}}
+\define@key{mdef}{s}{\def\@mdsuffix{#1}}
+\define@key{mdef}{arg}{\def\@mdargs{#1}}
+\define@key{mdef}{args}{\def\@mdargs{#1}}
+\define@boolkeys{mdef}{long,global}[true]
+\presetkeys{mdef}
+           {p=,s=,prefix=,suffix=,long=false,global=false,arg=0,args=0}{}
+\def\@mdef@az{a-z}
+\def\@mdef@AZ{A-Z}
+\def\@mdef@alphabet{a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z}
+\def\@mdef@Alphabet{A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z}
+\newcommand\multidef[3][]{%
+  \setkeys{mdef}{#1}%
+  \def\@mdef@com##1{#2}%
+  \@mdef#3,\@end}
+\def\@mdef #1,#2\@end{\expandafter\def\expandafter\@arg
+    \expandafter{\romannumeral-\expandafter`\expandafter\.#1}%
+  \ifx\@arg\@mdef@az
+    \expandafter\@mdef \@mdef@alphabet,\@end
+  \else
+    \ifx\@arg\@mdef@AZ
+      \expandafter\@mdef \@mdef@Alphabet,\@end
+    \else
+      \expandafter\@@mdef\@arg->->->\@end
+    \fi
+  \fi
+  \def\@arg{#2}%
+  \ifx\@arg\@empty\else\@mdef #2\@end\fi}
+\newtoks\@mdef@redeftok
+\def\@mdef@comma{}
+\def\@@mdef#1->#2->#3\@end{%
+  \@ifundefined{\@mdprefix#1\@mdsuffix}
+    {\@@@mdef{#1}{#2}}
+    {\edef\@mdef@redef{\the\@mdef@redeftok\@mdef@comma
+        \@backslashchar\@mdprefix#1\@mdsuffix}
+     \def\@mdef@comma{, }
+     \@mdef@redeftok=\expandafter{\@mdef@redef}
+     \ifKV@mdef@noerr
+       \@@@mdef{#1}{#2}%
+       \ifKV@mdef@nowarn\else
+         \PackageWarning{multidef}
+           {command \expandafter\noexpand\csname\@mdprefix#1\@mdsuffix\endcsname
+             redefined}
+       \fi
+     \else
+       \PackageError{multidef}
+         {command \expandafter\noexpand\csname\@mdprefix#1\@mdsuffix\endcsname
+           already defined}\@ehc
+     \fi
+     \ifKV@mdef@nowarn\else
+       \@ifundefined{@mdwarnonce}
+         {\def\@mdwarnonce{}%
+          \@mdef@finalwarn}
+         {}
+     \fi}
+}
+\def\@mdef@finalwarn{%
+  \AtEndDocument{\PackageWarningNoLine{multidef}{There were
+     redefined commands (\the\@mdef@redeftok)}}}
+\def\@@@mdef#1#2{\def\@arg@{#2}%
+  \ifx\@arg@\@empty
+    \@mdef@def{#1}{#1}%
+  \else
+    \@mdef@def{#1}{#2}%
+  \fi}
+\def\@mdef@def#1#2{%
+    \let\reserved@b\@gobble
+    \ifKV@mdef@global\let\@mdglobal\global\else\let\@mdglobal\relax\fi
+    \ifKV@mdef@long\let\@mdlong\long\else\let\@mdlong\relax\fi
+    \def\l@ngrel@x{\@mdlong\@mdglobal}
+  \expandafter\expandafter\expandafter\@yargd@f\expandafter\@mdargs\csname
+  \@mdprefix#1\@mdsuffix\expandafter\endcsname\expandafter{\@mdef@com{#2}}
+}
+%% 
+%%
+%% End of file `multidef.sty'.
diff --git a/thys/Delta_System_Lemma/document/root.bib b/thys/Delta_System_Lemma/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/document/root.bib
@@ -0,0 +1,81 @@
+@article{DBLP:journals/jar/PaulsonG96,
+  author    = {Lawrence C. Paulson and
+               Krzysztof Grabczewski},
+  title     = {Mechanizing Set Theory},
+  journal   = {J. Autom. Reasoning},
+  volume    = {17},
+  number    = {3},
+  pages     = {291--323},
+  year      = {1996},
+  xurl       = {https://doi.org/10.1007/BF00283132},
+  doi       = {10.1007/BF00283132},
+  timestamp = {Sat, 20 May 2017 00:22:31 +0200},
+  biburl    = {https://dblp.org/rec/bib/journals/jar/PaulsonG96},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{2020arXiv200109715G,
+       author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
+        title = "{Formalization of Forcing in Isabelle/ZF}",
+    isbn      = {978-3-662-45488-6},
+    booktitle = {Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1--4, 2020, Proceedings, Part II},
+    volume    = 12167,
+    series    = {Lecture Notes in Artificial Intelligence},
+    editor    = {Peltier, Nicolas and  Sofronie-Stokkermans, Viorica},
+    publisher = {Springer International Publishing},
+    doi       = {10.1007/978-3-030-51054-1},
+    pages     = {221--235},
+     keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1},
+         year = 2020,
+          eid = {arXiv:2001.09715},
+archivePrefix = {arXiv},
+       eprint = {2001.09715},
+ primaryClass = {cs.LO},
+       adsurl = {https://ui.adsabs.harvard.edu/abs/2020arXiv200109715G},
+     abstract = {We formalize the theory of forcing in the set theory framework of
+Isabelle/ZF. Under the assumption of the existence of a countable
+transitive model of $\mathit{ZFC}$, we construct a proper generic extension and show
+that the latter also satisfies $\mathit{ZFC}$. In doing so, we remodularized
+Paulson's ZF-Constructibility library.},
+      adsnote = {Provided by the SAO/NASA Astrophysics Data System}
+}
+
+@Book{Jech_Millennium,
+    author =	"Thomas Jech",
+    title =	"Set Theory. The Millennium Edition",
+    series =	"Springer Monographs in Mathematics",
+    publisher = "Springer-Verlag",
+    edition = "Third",
+    year =	"2002",
+    note = {Corrected fourth printing, 2006}
+}
+
+@misc{apunte_st,
+  author = {S{\'a}nchez Terraf, Pedro},
+  title = "Course notes on set theory",
+  howpublished = {online},
+  year = 2019,
+  note = "In Spanish",
+  url = {https://cs.famaf.unc.edu.ar/~pedro/home_en.html#set_theory}
+}
+
+@book{kunen2011set,
+  title={Set Theory},
+  author={Kunen, K.},
+  edition = {Second},
+  isbn=9781848900509,
+  series={Studies in Logic},
+  url={https://books.google.com.ar/books?id=Zn8ppwAACAAJ},
+  year=2011,
+  publisher={College Publications},
+  note = {Revised edition, 2013}
+}
+
+@Book{JW,
+    author =	"Winfried Just and Martin Weese",
+    title =	"Discovering Modern Set Theory. II",
+    series =	"Grad. Studies in Mathematics",
+    volume =	"18",
+    publisher = "American Mathematical Society", 
+    year =	"1997"
+}
diff --git a/thys/Delta_System_Lemma/document/root.bst b/thys/Delta_System_Lemma/document/root.bst
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/document/root.bst
@@ -0,0 +1,1561 @@
+%% 
+%% by pedro
+%% Based on file `model1b-num-names.bst'
+%% 
+%%
+%%
+ENTRY
+  { address
+    archive
+    author
+    booktitle
+    chapter
+    doi
+    edition
+    editor
+    eid
+    eprint
+    howpublished
+    institution
+    journal
+    key
+    month
+    note
+    number
+    organization
+    pages
+    publisher
+    school
+    series
+    title
+    type
+    url
+    volume
+    year
+    zbl
+  }
+  {}
+  { label extra.label sort.label short.list }
+INTEGERS { output.state before.all mid.sentence after.sentence after.block }
+FUNCTION {init.state.consts}
+{ #0 'before.all :=
+  #1 'mid.sentence :=
+  #2 'after.sentence :=
+  #3 'after.block :=
+}
+STRINGS { s t}
+FUNCTION {output.nonnull}
+{ 's :=
+  output.state mid.sentence =
+    { ", " * write$ }
+    { output.state after.block =
+        { add.period$ write$
+          newline$
+          "\newblock " write$
+        }
+        { output.state before.all =
+            'write$
+            { add.period$ " " * write$ }
+          if$
+        }
+      if$
+      mid.sentence 'output.state :=
+    }
+  if$
+  s
+}
+FUNCTION {output}
+{ duplicate$ empty$
+    'pop$
+    'output.nonnull
+  if$
+}
+FUNCTION {output.check}
+{ 't :=
+  duplicate$ empty$
+    { pop$ "empty " t * " in " * cite$ * warning$ }
+    'output.nonnull
+  if$
+}
+FUNCTION {fin.entry}
+{ add.period$
+  write$
+  newline$
+}
+
+FUNCTION {new.block}
+{ output.state before.all =
+    'skip$
+    { after.block 'output.state := }
+  if$
+}
+FUNCTION {new.sentence}
+{ output.state after.block =
+    'skip$
+    { output.state before.all =
+        'skip$
+        { after.sentence 'output.state := }
+      if$
+    }
+  if$
+}
+FUNCTION {add.blank}
+{  " " * before.all 'output.state :=
+}
+
+FUNCTION {date.block}
+{
+  skip$
+}
+
+FUNCTION {not}
+{   { #0 }
+    { #1 }
+  if$
+}
+FUNCTION {and}
+{   'skip$
+    { pop$ #0 }
+  if$
+}
+FUNCTION {or}
+{   { pop$ #1 }
+    'skip$
+  if$
+}
+FUNCTION {new.block.checkb}
+{ empty$
+  swap$ empty$
+  and
+    'skip$
+    'new.block
+  if$
+}
+FUNCTION {field.or.null}
+{ duplicate$ empty$
+    { pop$ "" }
+    'skip$
+  if$
+}
+FUNCTION {emphasize}
+{ duplicate$ empty$
+    { pop$ "" }
+    { "\textit{" swap$ * "}" * }
+  if$
+}
+%% by pedro
+FUNCTION {slanted}
+{ duplicate$ empty$
+    { pop$ "" }
+    { "\textsl{" swap$ * "}" * }
+  if$
+}
+FUNCTION {smallcaps}
+{ duplicate$ empty$
+    { pop$ "" }
+    { "\textsc{" swap$ * "}" * }
+  if$
+}
+FUNCTION {bold}
+{ duplicate$ empty$
+    { pop$ "" }
+    { "\textbf{" swap$ * "}" * }
+  if$
+}
+
+
+FUNCTION {tie.or.space.prefix}
+{ duplicate$ text.length$ #3 <
+    { "~" }
+    { " " }
+  if$
+  swap$
+}
+
+FUNCTION {capitalize}
+{ "u" change.case$ "t" change.case$ }
+
+FUNCTION {space.word}
+{ " " swap$ * " " * }
+ % Here are the language-specific definitions for explicit words.
+ % Each function has a name bbl.xxx where xxx is the English word.
+ % The language selected here is ENGLISH
+FUNCTION {bbl.and}
+{ "and"}
+
+FUNCTION {bbl.etal}
+{ "et~al." }
+
+FUNCTION {bbl.editors}
+{ "eds." }
+
+FUNCTION {bbl.editor}
+{ "ed." }
+
+FUNCTION {bbl.edby}
+{ "edited by" }
+
+FUNCTION {bbl.edition}
+{ "edition" }
+
+FUNCTION {bbl.volume}
+{ "volume" }
+
+FUNCTION {bbl.of}
+{ "of" }
+
+FUNCTION {bbl.number}
+{ "number" }
+
+FUNCTION {bbl.nr}
+{ "no." }
+
+FUNCTION {bbl.in}
+{ "in" }
+
+FUNCTION {bbl.pages}
+{ "pp." }
+
+FUNCTION {bbl.page}
+{ "p." }
+
+FUNCTION {bbl.chapter}
+{ "chapter" }
+
+FUNCTION {bbl.techrep}
+{ "Technical Report" }
+
+FUNCTION {bbl.mthesis}
+{ "Master's thesis" }
+
+FUNCTION {bbl.phdthesis}
+{ "Ph.D. thesis" }
+
+FUNCTION {bbl.first}
+{ "1st" }
+
+FUNCTION {bbl.second}
+{ "2nd" }
+
+FUNCTION {bbl.third}
+{ "3rd" }
+
+FUNCTION {bbl.fourth}
+{ "4th" }
+
+FUNCTION {bbl.fifth}
+{ "5th" }
+
+FUNCTION {bbl.th}
+{ "th" }
+
+FUNCTION {bbl.st}
+{ "st" }
+
+FUNCTION {bbl.nd}
+{ "nd" }
+
+FUNCTION {bbl.rd}
+{ "rd" }
+
+MACRO {jan} {"January"}
+
+MACRO {feb} {"February"}
+
+MACRO {mar} {"March"}
+
+MACRO {apr} {"April"}
+
+MACRO {may} {"May"}
+
+MACRO {jun} {"June"}
+
+MACRO {jul} {"July"}
+
+MACRO {aug} {"August"}
+
+MACRO {sep} {"September"}
+
+MACRO {oct} {"October"}
+
+MACRO {nov} {"November"}
+
+MACRO {dec} {"December"}
+
+FUNCTION {eng.ord}
+{ duplicate$ "1" swap$ *
+  #-2 #1 substring$ "1" =
+     { bbl.th * }
+     { duplicate$ #-1 #1 substring$
+       duplicate$ "1" =
+         { pop$ bbl.st * }
+         { duplicate$ "2" =
+             { pop$ bbl.nd * }
+             { "3" =
+                 { bbl.rd * }
+                 { bbl.th * }
+               if$
+             }
+           if$
+          }
+       if$
+     }
+   if$
+}
+
+MACRO {acmcs} {"ACM Comput. Surv."}
+
+MACRO {acta} {"Acta Inf."}
+
+MACRO {cacm} {"Commun. ACM"}
+
+MACRO {ibmjrd} {"IBM J. Res. Dev."}
+
+MACRO {ibmsj} {"IBM Syst.~J."}
+
+MACRO {ieeese} {"IEEE Trans. Software Eng."}
+
+MACRO {ieeetc} {"IEEE Trans. Comput."}
+
+MACRO {ieeetcad}
+ {"IEEE Trans. Comput. Aid. Des."}
+
+MACRO {ipl} {"Inf. Process. Lett."}
+
+MACRO {jacm} {"J.~ACM"}
+
+MACRO {jcss} {"J.~Comput. Syst. Sci."}
+
+MACRO {scp} {"Sci. Comput. Program."}
+
+MACRO {sicomp} {"SIAM J. Comput."}
+
+MACRO {tocs} {"ACM Trans. Comput. Syst."}
+
+MACRO {tods} {"ACM Trans. Database Syst."}
+
+MACRO {tog} {"ACM Trans. Graphic."}
+
+MACRO {toms} {"ACM Trans. Math. Software"}
+
+MACRO {toois} {"ACM Trans. Office Inf. Syst."}
+
+MACRO {toplas} {"ACM Trans. Progr. Lang. Syst."}
+
+MACRO {tcs} {"Theor. Comput. Sci."}
+
+FUNCTION {bibinfo.check}
+{ swap$
+  duplicate$ missing$
+    {
+      pop$ pop$
+      ""
+    }
+    { duplicate$ empty$
+        {
+          swap$ pop$
+        }
+        { swap$
+          "\bibinfo{" swap$ * "}{" * swap$ * "}" *
+        }
+      if$
+    }
+  if$
+}
+FUNCTION {bibinfo.warn}
+{ swap$
+  duplicate$ missing$
+    {
+      swap$ "missing " swap$ * " in " * cite$ * warning$ pop$
+      ""
+    }
+    { duplicate$ empty$
+        {
+          swap$ "empty " swap$ * " in " * cite$ * warning$
+        }
+        { swap$
+          pop$
+        }
+      if$
+    }
+  if$
+}
+FUNCTION {format.zbl}
+{ zbl empty$
+    { "" }
+%    { "\urlprefix\url{" url * "}" * }
+    { "\zbl{" zbl * "}" * }  % changed in titto-lncs-02.bst
+  if$
+}
+FUNCTION {format.url}
+{ url empty$
+    { "" }
+%    { "\urlprefix\url{" url * "}" * }
+    { "\url{" url * "}" * }  % changed in titto-lncs-02.bst
+  if$
+}
+
+FUNCTION {format.doi} % added in splncs04.bst
+{ doi empty$
+     { "" }
+     { after.block 'output.state :=
+       "\doi{" doi * "}" * }
+  if$
+}
+
+FUNCTION {format.eprint}
+{ eprint duplicate$ empty$
+    'skip$
+    { "\eprint"
+      archive empty$
+        'skip$
+        { "[" * archive * "]" * }
+      if$
+      "{" * swap$ * "}" *
+    }
+  if$
+}
+
+STRINGS  { bibinfo}
+INTEGERS { nameptr namesleft numnames }
+
+FUNCTION {format.names}
+{ 'bibinfo :=
+  duplicate$ empty$ 'skip$ {
+  's :=
+  "" 't :=
+  #1 'nameptr :=
+  s num.names$ 'numnames :=
+  numnames 'namesleft :=
+    { namesleft #0 > }
+    { s nameptr
+      "{f{.}.~}{vv~}{ll}{, jj}"
+      format.name$
+      bibinfo bibinfo.check
+      't :=
+      nameptr #1 >
+        {
+          namesleft #1 >
+            { ", " * t * }
+            {
+              "," *
+              s nameptr "{ll}" format.name$ duplicate$ "others" =
+                { 't := }
+                { pop$ }
+              if$
+              t "others" =
+                {
+                  " " * bbl.etal *
+                }
+                { " " * t * }
+              if$
+            }
+          if$
+        }
+        't
+      if$
+      nameptr #1 + 'nameptr :=
+      namesleft #1 - 'namesleft :=
+    }
+  while$
+  } if$
+}
+FUNCTION {format.names.ed}
+{
+  format.names
+}
+FUNCTION {format.key}
+{ empty$
+    { key field.or.null }
+    { "" }
+  if$
+}
+
+FUNCTION {format.authors}
+{ author "author" format.names smallcaps
+}
+FUNCTION {get.bbl.editor}
+{ editor num.names$ #1 > 'bbl.editors 'bbl.editor if$ }
+
+FUNCTION {format.editors}
+{ editor "editor" format.names duplicate$ empty$ 'skip$
+    {
+      " " *
+      get.bbl.editor
+      capitalize
+   "(" swap$ * ")" *
+      *
+    }
+  if$
+}
+FUNCTION {format.note}
+{
+ note empty$
+    { "" }
+    { note #1 #1 substring$
+      duplicate$ "{" =
+        'skip$
+        { output.state mid.sentence =
+          { "l" }
+          { "u" }
+        if$
+        change.case$
+        }
+      if$
+      note #2 global.max$ substring$ * "note" bibinfo.check
+    }
+  if$
+}
+
+FUNCTION {format.title}
+{ title
+  duplicate$ empty$ 'skip$
+    { "t" change.case$ }
+  if$
+  "title" bibinfo.check
+}
+FUNCTION {format.full.names}
+{'s :=
+ "" 't :=
+  #1 'nameptr :=
+  s num.names$ 'numnames :=
+  numnames 'namesleft :=
+    { namesleft #0 > }
+    { s nameptr
+      "{vv~}{ll}" format.name$
+      't :=
+      nameptr #1 >
+        {
+          namesleft #1 >
+            { ", " * t * }
+            {
+              s nameptr "{ll}" format.name$ duplicate$ "others" =
+                { 't := }
+                { pop$ }
+              if$
+              t "others" =
+                {
+                  " " * bbl.etal *
+                }
+                {
+                  bbl.and
+                  space.word * t *
+                }
+              if$
+            }
+          if$
+        }
+        't
+      if$
+      nameptr #1 + 'nameptr :=
+      namesleft #1 - 'namesleft :=
+    }
+  while$
+}
+
+FUNCTION {author.editor.key.full}
+{ author empty$
+    { editor empty$
+        { key empty$
+            { cite$ #1 #3 substring$ }
+            'key
+          if$
+        }
+        { editor format.full.names }
+      if$
+    }
+    { author format.full.names }
+  if$
+}
+
+FUNCTION {author.key.full}
+{ author empty$
+    { key empty$
+         { cite$ #1 #3 substring$ }
+          'key
+      if$
+    }
+    { author format.full.names }
+  if$
+}
+
+FUNCTION {editor.key.full}
+{ editor empty$
+    { key empty$
+         { cite$ #1 #3 substring$ }
+          'key
+      if$
+    }
+    { editor format.full.names }
+  if$
+}
+
+FUNCTION {make.full.names}
+{ type$ "book" =
+  type$ "inbook" =
+  or
+    'author.editor.key.full
+    { type$ "proceedings" =
+        'editor.key.full
+        'author.key.full
+      if$
+    }
+  if$
+}
+
+FUNCTION {output.bibitem}
+{ newline$
+  "\bibitem[{" write$
+  label write$
+  ")" make.full.names duplicate$ short.list =
+     { pop$ }
+     { * }
+   if$
+  "}]{" * write$
+  cite$ write$
+  "}" write$
+  newline$
+  ""
+  before.all 'output.state :=
+}
+
+FUNCTION {n.dashify}
+{
+  't :=
+  ""
+    { t empty$ not }
+    { t #1 #1 substring$ "-" =
+        { t #1 #2 substring$ "--" = not
+            { "--" *
+              t #2 global.max$ substring$ 't :=
+            }
+            {   { t #1 #1 substring$ "-" = }
+                { "-" *
+                  t #2 global.max$ substring$ 't :=
+                }
+              while$
+            }
+          if$
+        }
+        { t #1 #1 substring$ *
+          t #2 global.max$ substring$ 't :=
+        }
+      if$
+    }
+  while$
+}
+
+FUNCTION {word.in}
+{ bbl.in
+  ":" *
+  " " * }
+
+FUNCTION {format.date}
+{ year "year" bibinfo.check duplicate$ empty$
+    {
+      "empty year in " cite$ * "; set to ????" * warning$
+       pop$ "????"
+    }
+    'skip$
+  if$
+  %  extra.label *
+  %% by pedro
+  " (" swap$ * ")" *
+}
+FUNCTION{format.year}
+{ year "year" bibinfo.check duplicate$ empty$
+    {  "empty year in " cite$ *
+       "; set to ????" *
+       warning$
+       pop$ "????"
+    }
+    {
+    }
+  if$
+  % extra.label *
+  " (" swap$ * ")" *
+}
+FUNCTION {format.btitle}
+{ title "title" bibinfo.check
+  duplicate$ empty$ 'skip$
+    {
+    }
+  if$
+  %% by pedro
+  "``" swap$ * "''" *
+}
+FUNCTION {either.or.check}
+{ empty$
+    'pop$
+    { "can't use both " swap$ * " fields in " * cite$ * warning$ }
+  if$
+}
+FUNCTION {format.bvolume}
+{ volume empty$
+    { "" }
+    %% by pedro
+    { series "series" bibinfo.check
+      duplicate$ empty$ 'pop$
+        { %slanted
+           }
+      if$
+      "volume and number" number either.or.check
+      volume tie.or.space.prefix
+      "volume" bibinfo.check 
+      bold
+      * *
+    }
+  if$
+}
+FUNCTION {format.number.series}
+{ volume empty$
+    { number empty$
+        { series field.or.null }
+        { series empty$
+            { number "number" bibinfo.check }
+        { output.state mid.sentence =
+            { bbl.number }
+            { bbl.number capitalize }
+          if$
+          number tie.or.space.prefix "number" bibinfo.check * *
+          bbl.in space.word *
+          series "series" bibinfo.check *
+        }
+      if$
+    }
+      if$
+    }
+    { "" }
+  if$
+}
+
+FUNCTION {format.edition}
+{ edition duplicate$ empty$ 'skip$
+    {
+      output.state mid.sentence =
+        { "l" }
+        { "t" }
+      if$ change.case$
+      "edition" bibinfo.check
+      " " * bbl.edition *
+    }
+  if$
+}
+
+INTEGERS { multiresult }
+FUNCTION {multi.page.check}
+{ 't :=
+  #0 'multiresult :=
+    { multiresult not
+      t empty$ not
+      and
+    }
+    { t #1 #1 substring$
+      duplicate$ "-" =
+      swap$ duplicate$ "," =
+      swap$ "+" =
+      or or
+        { #1 'multiresult := }
+        { t #2 global.max$ substring$ 't := }
+      if$
+    }
+  while$
+  multiresult
+}
+FUNCTION {format.pages}
+{ pages duplicate$ empty$ 'skip$
+    { duplicate$ multi.page.check
+        {
+          bbl.pages swap$
+          n.dashify
+        }
+        {
+          bbl.page swap$
+        }
+      if$
+      tie.or.space.prefix
+      "pages" bibinfo.check
+      * *
+    }
+  if$
+}
+
+FUNCTION {format.pages.simple}
+{ pages duplicate$ empty$ 'skip$
+    { duplicate$ multi.page.check
+        {
+%          bbl.pages swap$
+          n.dashify
+        }
+        {
+%          bbl.page swap$
+        }
+      if$
+      tie.or.space.prefix
+      "pages" bibinfo.check
+      * 
+    }
+  if$
+}
+FUNCTION {format.journal.pages}
+{ pages duplicate$ empty$ 'pop$
+    { swap$ duplicate$ empty$
+        { pop$ pop$ format.pages }
+        {
+          ": " *
+          swap$
+          n.dashify
+          "pages" bibinfo.check
+          *
+        }
+      if$
+    }
+  if$
+}
+FUNCTION {format.vol.num.pages}
+{ volume field.or.null
+  duplicate$ empty$ 'skip$
+    {
+      "volume" bibinfo.check
+    }
+  if$
+  %% by pedro
+  bold
+  pages duplicate$ empty$ 'pop$
+  { swap$ duplicate$ empty$
+      { pop$ pop$ format.pages }
+      {
+        ": " *
+        swap$
+        n.dashify
+        "pages" bibinfo.check
+        *
+      }
+      if$
+  }
+  if$
+  format.year * 
+}
+
+FUNCTION {format.chapter.pages}
+{ chapter empty$
+    { "" }
+    { type empty$
+        { bbl.chapter }
+        { type "l" change.case$
+          "type" bibinfo.check
+        }
+      if$
+      chapter tie.or.space.prefix
+      "chapter" bibinfo.check
+      * *
+    }
+  if$
+}
+
+FUNCTION {format.booktitle}
+{
+  booktitle "booktitle" bibinfo.check
+}
+FUNCTION {format.in.ed.booktitle}
+{ format.booktitle duplicate$ empty$ 'skip$
+    {
+      editor "editor" format.names.ed duplicate$ empty$ 'pop$
+        {
+          " " *
+          get.bbl.editor
+          capitalize
+          "(" swap$ * "), " *
+          * swap$
+          * }
+      if$
+      word.in swap$ *
+    }
+  if$
+}
+FUNCTION {format.thesis.type}
+{ type duplicate$ empty$
+    'pop$
+    { swap$ pop$
+      "t" change.case$ "type" bibinfo.check
+    }
+  if$
+}
+FUNCTION {format.tr.number}
+{ number "number" bibinfo.check
+  type duplicate$ empty$
+    { pop$ bbl.techrep }
+    'skip$
+  if$
+  "type" bibinfo.check
+  swap$ duplicate$ empty$
+    { pop$ "t" change.case$ }
+    { tie.or.space.prefix * * }
+  if$
+}
+FUNCTION {format.article.crossref}
+{
+  word.in
+  " \cite{" * crossref * "}" *
+}
+FUNCTION {format.book.crossref}
+{ volume duplicate$ empty$
+    { "empty volume in " cite$ * "'s crossref of " * crossref * warning$
+      pop$ word.in
+    }
+    { bbl.volume
+      swap$ tie.or.space.prefix "volume" bibinfo.check * * bbl.of space.word *
+    }
+  if$
+  " \cite{" * crossref * "}" *
+}
+FUNCTION {format.incoll.inproc.crossref}
+{
+  word.in
+  " \cite{" * crossref * "}" *
+}
+FUNCTION {format.org.or.pub}
+{ 't :=
+  ""
+  address empty$ t empty$ and
+    'skip$
+    {
+      t empty$
+        { address "address" bibinfo.check *
+        }
+        { t *
+          address empty$
+            'skip$
+            { ", " * address "address" bibinfo.check * }
+          if$
+        }
+      if$
+    }
+  if$
+}
+FUNCTION {format.publisher.address}
+{ publisher "publisher" bibinfo.check format.org.or.pub
+}
+FUNCTION {format.publisher.address.year}
+{ publisher "publisher" bibinfo.check format.org.or.pub
+  format.journal.pages
+  format.year *
+}
+
+FUNCTION {school.address.year}
+{ school "school"  bibinfo.warn 
+  address empty$
+    'skip$
+    { ", " * address "address" bibinfo.check * }
+  if$
+ format.year * 
+}
+
+FUNCTION {format.publisher.address.pages}
+{ publisher "publisher" bibinfo.check format.org.or.pub
+  format.year *
+  
+}
+
+FUNCTION {format.organization.address}
+{ organization "organization" bibinfo.check format.org.or.pub
+}
+
+FUNCTION {format.organization.address.year}
+{ organization "organization" bibinfo.check format.org.or.pub
+  format.journal.pages
+  format.year *
+}
+
+FUNCTION {article}
+{ "%Type = Article" write$
+  output.bibitem
+  format.authors "author" output.check
+  author format.key output
+  format.title "title" output.check
+  crossref missing$
+    {
+      journal
+      "journal" bibinfo.check
+      %% by pedro
+      emphasize
+      "journal" output.check
+      add.blank
+      format.vol.num.pages output
+    }
+    { format.article.crossref output.nonnull
+    }
+  if$
+%  format.journal.pages
+  new.sentence
+  format.note output
+  format.doi output
+  fin.entry
+}
+FUNCTION {book}
+{ "%Type = Book" write$
+  output.bibitem
+  author empty$
+    { format.editors "author and editor" output.check
+      editor format.key output
+    }
+    { format.authors output.nonnull
+      crossref missing$
+        { "author and editor" editor either.or.check }
+        'skip$
+      if$
+    }
+  if$
+  format.btitle "title" output.check
+  crossref missing$
+    { %% by pedro
+      format.bvolume output
+      format.number.series output
+      % format.bvolume output
+      format.publisher.address.year output
+    }
+    {
+      format.book.crossref output.nonnull
+    }
+  if$
+  format.edition output
+  % format.date "year" output.check
+  new.sentence
+  format.note output
+  format.doi output
+  format.eprint output
+  fin.entry
+}
+FUNCTION {booklet}
+{ "%Type = Booklet" write$
+  output.bibitem
+  format.authors output
+  author format.key output
+  format.title "title" output.check
+  howpublished "howpublished" bibinfo.check output
+  address "address" bibinfo.check output
+  format.date "year" output.check
+  new.sentence
+  format.note output
+  format.doi output
+  format.eprint output
+  fin.entry
+}
+
+FUNCTION {inbook}
+{ "%Type = Inbook" write$
+  output.bibitem
+  author empty$
+    { format.editors "author and editor" output.check
+      editor format.key output
+    }
+    { format.authors output.nonnull
+  format.title "title" output.check
+      crossref missing$
+        { "author and editor" editor either.or.check }
+        'skip$
+      if$
+    }
+  if$
+  format.btitle "title" output.check
+  crossref missing$
+    {
+      format.bvolume output
+      format.number.series output
+      format.publisher.address output
+      format.pages "pages" output.check
+      format.edition output
+      format.date "year" output.check
+    }
+    {
+      format.book.crossref output.nonnull
+    }
+  if$
+%  format.edition output
+%  format.pages "pages" output.check
+  new.sentence
+  format.note output
+  format.doi output
+  fin.entry
+}
+
+FUNCTION {incollection}
+{ "%Type = Incollection" write$
+  output.bibitem
+  format.authors "author" output.check
+  author format.key output
+  format.title "title" output.check
+  crossref missing$
+    { format.in.ed.booktitle "booktitle" output.check
+      format.bvolume output
+      format.number.series output
+      format.pages "pages" output.check
+      % format.publisher.address output
+      % format.date "year" output.check
+      format.publisher.address.year output
+      format.edition output
+    }
+    { format.incoll.inproc.crossref output.nonnull
+    }
+  if$
+%  format.pages "pages" output.check
+  new.sentence
+  format.note output
+  format.doi output
+  fin.entry
+}
+FUNCTION {inproceedings}
+{ "%Type = Inproceedings" write$
+  output.bibitem
+  format.authors "author" output.check
+  author format.key output
+  format.title "title" output.check
+  crossref missing$
+    {
+      journal
+      "journal" bibinfo.check
+      "journal" output.check
+      format.in.ed.booktitle "booktitle" output.check
+      format.bvolume output
+      format.number.series output
+      publisher empty$
+        { %format.organization.address output 
+	  format.organization.address.year output 
+%	  format.journal.pages		  
+	}
+        { organization "organization" bibinfo.check output
+          format.publisher.address.year output
+          % format.date "year" output.check
+%	  format.journal.pages
+        }
+      if$
+    }
+    { format.incoll.inproc.crossref output.nonnull
+      format.journal.pages
+    }
+  if$
+% format.pages.simple "pages" output.check
+%%% La que sigue la muevo adentro del "if"
+% format.journal.pages
+  new.sentence
+  format.note output
+  format.doi output
+  fin.entry
+}
+FUNCTION {conference} { inproceedings }
+FUNCTION {manual}
+{ "%Type = Manual" write$
+  output.bibitem
+  format.authors output
+  author format.key output
+  format.btitle "title" output.check
+  organization "organization" bibinfo.check output
+  address "address" bibinfo.check output
+  format.edition output
+  format.date "year" output.check
+  new.sentence
+  format.note output
+  format.doi output
+  format.eprint output
+  fin.entry
+}
+
+FUNCTION {mastersthesis}
+{ "%Type = Masterthesis" write$
+  output.bibitem
+  format.authors "author" output.check
+  author format.key output
+  format.btitle
+  "title" output.check
+  bbl.mthesis format.thesis.type output.nonnull
+%  school "school" bibinfo.warn output
+%  address "address" bibinfo.check output
+%  format.date "year" output.check
+  school.address.year output
+  new.sentence
+  format.note output
+  format.doi output
+  format.eprint output
+  fin.entry
+}
+
+FUNCTION {misc}
+{ "%Type = Misc" write$
+  output.bibitem
+  format.authors output
+  author format.key output
+  format.title output
+  howpublished "howpublished" bibinfo.check output
+  format.date "year" output.check
+  new.sentence
+  format.note output
+  format.url output
+  format.doi output
+  format.eprint output
+  new.block
+  fin.entry
+}
+FUNCTION {phdthesis}
+{ "%Type = Phdthesis" write$
+  output.bibitem
+  format.authors "author" output.check
+  author format.key output
+  format.btitle
+  "title" output.check
+  bbl.phdthesis format.thesis.type output.nonnull
+%  school "school" bibinfo.warn output
+%  address "address" bibinfo.check output
+%  format.date "year" output.check
+  school.address.year output
+  new.sentence
+  format.note output
+  format.doi output
+  format.eprint output
+  fin.entry
+}
+
+FUNCTION {proceedings}
+{ "%Type = Proceedings" write$
+  output.bibitem
+  format.editors output
+  editor format.key output
+  format.btitle "title" output.check
+  format.bvolume output
+  format.number.series output
+  publisher empty$
+    { format.organization.address output }
+    { organization "organization" bibinfo.check output
+      format.publisher.address output
+    }
+  if$
+  format.date "year" output.check
+  new.sentence
+  format.note output
+  format.doi output
+  fin.entry
+}
+
+FUNCTION {techreport}
+{ "%Type = Techreport" write$
+  output.bibitem
+  format.authors "author" output.check
+  author format.key output
+  format.btitle
+  "title" output.check
+  format.tr.number output.nonnull
+  institution "institution" bibinfo.warn output
+  address "address" bibinfo.check output
+  format.date "year" output.check
+  new.sentence
+  format.note output
+  format.url output
+  format.doi output
+  format.eprint output
+  fin.entry
+}
+
+FUNCTION {unpublished}
+{ "%Type = Unpublished" write$
+  output.bibitem
+  format.authors "author" output.check
+  author format.key output
+  format.title "title" output.check
+  format.date "year" output.check
+  new.sentence
+  format.note "note" output.check
+  format.url output
+  format.doi output
+  format.eprint output
+  fin.entry
+}
+
+FUNCTION {default.type} { misc }
+READ
+FUNCTION {sortify}
+{ purify$
+  "l" change.case$
+}
+INTEGERS { len }
+FUNCTION {chop.word}
+{ 's :=
+  'len :=
+  s #1 len substring$ =
+    { s len #1 + global.max$ substring$ }
+    's
+  if$
+}
+FUNCTION {format.lab.names}
+{ 's :=
+  "" 't :=
+  s #1 "{vv~}{ll}" format.name$
+  s num.names$ duplicate$
+  #2 >
+    { pop$
+      " " * bbl.etal *
+    }
+    { #2 <
+        'skip$
+        { s #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =
+            {
+              " " * bbl.etal *
+            }
+            { bbl.and space.word * s #2 "{vv~}{ll}" format.name$
+              * }
+          if$
+        }
+      if$
+    }
+  if$
+}
+
+FUNCTION {author.key.label}
+{ author empty$
+    { key empty$
+        { cite$ #1 #3 substring$ }
+        'key
+      if$
+    }
+    { author format.lab.names }
+  if$
+}
+
+FUNCTION {author.editor.key.label}
+{ author empty$
+    { editor empty$
+        { key empty$
+            { cite$ #1 #3 substring$ }
+            'key
+          if$
+        }
+        { editor format.lab.names }
+      if$
+    }
+    { author format.lab.names }
+  if$
+}
+
+FUNCTION {editor.key.label}
+{ editor empty$
+    { key empty$
+        { cite$ #1 #3 substring$ }
+        'key
+      if$
+    }
+    { editor format.lab.names }
+  if$
+}
+
+FUNCTION {calc.short.authors}
+{ type$ "book" =
+  type$ "inbook" =
+  or
+    'author.editor.key.label
+    { type$ "proceedings" =
+        'editor.key.label
+        'author.key.label
+      if$
+    }
+  if$
+  'short.list :=
+}
+
+FUNCTION {calc.label}
+{ calc.short.authors
+  short.list
+  "("
+  *
+  year duplicate$ empty$
+     { pop$ "????" }
+     { purify$ #-1 #4 substring$ }
+  if$
+  *
+  'label :=
+}
+
+FUNCTION {sort.format.names}
+{ 's :=
+  #1 'nameptr :=
+  ""
+  s num.names$ 'numnames :=
+  numnames 'namesleft :=
+    { namesleft #0 > }
+    { s nameptr
+      "{ll{ }}{  f{ }}{  jj{ }}"
+      format.name$ 't :=
+      nameptr #1 >
+        {
+          "   "  *
+          namesleft #1 = t "others" = and
+            { "zzzzz" * }
+            { t sortify * }
+          if$
+        }
+        { t sortify * }
+      if$
+      nameptr #1 + 'nameptr :=
+      namesleft #1 - 'namesleft :=
+    }
+  while$
+}
+
+FUNCTION {sort.format.title}
+{ 't :=
+  "A " #2
+    "An " #3
+      "The " #4 t chop.word
+    chop.word
+  chop.word
+  sortify
+  #1 global.max$ substring$
+}
+FUNCTION {author.sort}
+{ author empty$
+    { key empty$
+        { "to sort, need author or key in " cite$ * warning$
+          ""
+        }
+        { key sortify }
+      if$
+    }
+    { author sort.format.names }
+  if$
+}
+FUNCTION {author.editor.sort}
+{ author empty$
+    { editor empty$
+        { key empty$
+            { "to sort, need author, editor, or key in " cite$ * warning$
+              ""
+            }
+            { key sortify }
+          if$
+        }
+        { editor sort.format.names }
+      if$
+    }
+    { author sort.format.names }
+  if$
+}
+FUNCTION {editor.sort}
+{ editor empty$
+    { key empty$
+        { "to sort, need editor or key in " cite$ * warning$
+          ""
+        }
+        { key sortify }
+      if$
+    }
+    { editor sort.format.names }
+  if$
+}
+FUNCTION {presort}
+{ calc.label
+  label sortify
+  "    "
+  *
+  type$ "book" =
+  type$ "inbook" =
+  or
+    'author.editor.sort
+    { type$ "proceedings" =
+        'editor.sort
+        'author.sort
+      if$
+    }
+  if$
+  #1 entry.max$ substring$
+  'sort.label :=
+  sort.label
+  *
+  "    "
+  *
+  title field.or.null
+  sort.format.title
+  *
+  #1 entry.max$ substring$
+  'sort.key$ :=
+}
+
+ITERATE {presort}
+SORT
+STRINGS { last.label next.extra }
+INTEGERS { last.extra.num number.label }
+FUNCTION {initialize.extra.label.stuff}
+{ #0 int.to.chr$ 'last.label :=
+  "" 'next.extra :=
+  #0 'last.extra.num :=
+  #0 'number.label :=
+}
+FUNCTION {forward.pass}
+{ last.label label =
+    { last.extra.num #1 + 'last.extra.num :=
+      last.extra.num int.to.chr$ 'extra.label :=
+    }
+    { "a" chr.to.int$ 'last.extra.num :=
+      "" 'extra.label :=
+      label 'last.label :=
+    }
+  if$
+  number.label #1 + 'number.label :=
+}
+FUNCTION {reverse.pass}
+{ next.extra "b" =
+    { "a" 'extra.label := }
+    'skip$
+  if$
+  extra.label 'next.extra :=
+  extra.label
+  duplicate$ empty$
+    'skip$
+    { "{\natexlab{" swap$ * "}}" * }
+  if$
+  'extra.label :=
+  label extra.label * 'label :=
+}
+EXECUTE {initialize.extra.label.stuff}
+ITERATE {forward.pass}
+REVERSE {reverse.pass}
+FUNCTION {bib.sort.order}
+{ sort.label
+  "    "
+  *
+  year field.or.null sortify
+  *
+  "    "
+  *
+  title field.or.null
+  sort.format.title
+  *
+  #1 entry.max$ substring$
+  'sort.key$ :=
+}
+ITERATE {bib.sort.order}
+SORT
+FUNCTION {begin.bib}
+{ preamble$ empty$
+    'skip$
+    { preamble$ write$ newline$ }
+  if$
+  "\begin{small}\begin{thebibliography}{" number.label int.to.str$ * "}" *
+  write$ newline$
+  "\expandafter\ifx\csname natexlab\endcsname\relax\def\natexlab#1{#1}\fi"
+  write$ newline$
+  "\providecommand{\bibinfo}[2]{#2}"
+  write$ newline$
+  "\providecommand{\doi}[1]{doi:\href{https://doi.org/#1}{#1}}"
+  write$ newline$
+ "\providecommand{\eprint}[2][]{arXiv:\href{https://arxiv.org/abs/#2}{#2}}"
+  write$ newline$
+  "\providecommand{\zbl}[1]{\hfill {\small Zbl~\href{https://zbmath.org/?q=an\%3A#1}{#1}}}"
+  write$ newline$
+	"\ifx\xfnm\relax \def\xfnm[#1]{\unskip,\space#1}\fi"
+  write$ newline$
+}
+EXECUTE {begin.bib}
+EXECUTE {init.state.consts}
+ITERATE {call.type$}
+FUNCTION {end.bib}
+{ newline$
+  "\end{thebibliography}\end{small}" write$ newline$
+}
+EXECUTE {end.bib}
diff --git a/thys/Delta_System_Lemma/document/root.tex b/thys/Delta_System_Lemma/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Delta_System_Lemma/document/root.tex
@@ -0,0 +1,119 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+\usepackage[numbers]{natbib}
+
+\usepackage{relsize}
+\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\itshape\smaller}
+\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
+\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\itshape\smaller}
+\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap]{stmaryrd}
+  %for \<Sqinter>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+\input{header-delta-system}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{tt}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+\renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
+\renewcommand{\isacharunderscore}{\mbox{\_}}
+\renewcommand{\isasymtturnstile}{\isamath{\Vdash}}
+\renewcommand{\isacharminus}{-}
+
+\begin{document}
+
+\title{Cofinality and the Delta System Lemma}
+\author{
+  Pedro S\'anchez Terraf\thanks{Universidad Nacional de C\'ordoba. 
+    Facultad de Matem\'atica, Astronom\'{\i}a,  F\'{\i}sica y
+    Computaci\'on.}
+  \thanks{%
+    Centro de Investigaci\'on y Estudios de Matem\'atica
+    (CIEM-FaMAF), Conicet. C\'ordoba. Argentina.
+    Supported by Secyt-UNC project 33620180100465CB.}
+}
+\maketitle
+
+\begin{abstract}
+  We formalize the basic results on cofinality of linearly ordered
+  sets and ordinals and \v{S}anin's Lemma for uncountable families of
+  finite sets. We work in the set theory framework of
+  Isabelle/ZF, using the Axiom of Choice as needed.
+\end{abstract}
+
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+\section{Introduction}
+
+The session we present gathers very basic results built on the set
+theory formalization of Isabelle/ZF
+\cite{DBLP:journals/jar/PaulsonG96}. In a sense, some of the material
+formalized here corresponds to a natural continuation of that
+work. This is even clearer after perusing Section~\ref{sec:zf-lib},
+where notions like cardinal exponentiation are first defined, together
+with various lemmas that do not depend on the Axiom of Choice ($\AC$);
+the same holds for the basic theory of cofinality of ordinals, which
+is developed in Section~\ref{sec:cofinality}. In
+Section~\ref{sec:cardinal-lib}, (un)countability is defined
+and several results proved, now using $\AC$ freely; the latter is also
+needed to prove König's Theorem on cofinality of cardinal
+exponentiation. The simplest infinitary version of the Delta
+System Lemma (DSL, also known as the ``Sunflower Lemma'') due to  \v{S}anin
+is proved in Section~\ref{sec:dsl}, and it is applied to prove
+that Cohen posets satisfy the \emph{countable chain condition}.
+
+A greater part of this development was motivated by an ongoing joint
+project on the formalization of the ctm approach to
+forcing~\cite{2020arXiv200109715G} by Gunther, Pagano, Steinberg, and
+the author. Indeed, most of the results presented here are required
+for the development of forcing. As it turns out, the material as
+formalized presently will not be part of the forcing formalization,
+since for that goal we need relativized versions of both the concepts
+and the proofs.
+
+A cross-linked HTML version of the development can be found at
+\url{https://cs.famaf.unc.edu.ar/~pedro/Delta_System_Lemma/html}.
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{root}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,572 +1,573 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BNF_CC
 BNF_Operations
 Banach_Steinhaus
 Bell_Numbers_Spivey
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CYK
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Consensus_Refined
 Constructive_Cryptography
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 DFS_Framework
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
+Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Harrison
 FOL_Seq_Calc1
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_SSA
 Formula_Derivatives
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interval_Arithmetic_Word32
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 Mersenne_Primes
 MiniML
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Projective_Geometry
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 UPF
 UPF_Firewall
 UTP
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 XML
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL