# Theory AC16_WO4

Up to index of Isabelle/ZF/AC

theory AC16_WO4
imports AC16_lemmas
begin

    (*  Title:      ZF/AC/AC16_WO4.thy
        ID:         $Id: AC16_WO4.thy,v 1.14 2005/06/17 14:15:10 haftmann Exp $
        Author:     Krzysztof Grabczewski

    The proof of AC16(n, k) ==> WO4(n-k)

    Tidied (using locales) by LCP
    *)

    theory AC16_WO4 imports AC16_lemmas begin

    (* ********************************************************************** *)
    (* The case of finite set                                                 *)
    (* ********************************************************************** *)

    lemma lemma1:
         "[| Finite(A); 0<m; m ∈ nat |]
          ==> ∃a f. Ord(a) & domain(f) = a &
                    (\<Union>b<a. f`b) = A & (∀b<a. f`b \<lesssim> m)"
    apply (unfold Finite_def)
    apply (erule bexE)
    apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
    apply (erule exE)
    apply (rule_tac x = n in exI)
    apply (rule_tac x = "λi ∈ n. {f`i}" in exI)
    apply (simp add: ltD bij_def surj_def)
    apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun]
                   singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
                        nat_1_lepoll_iff [THEN iffD2]
              elim!: apply_type ltE)
    done

    (* ********************************************************************** *)
    (* The case of infinite set                                               *)
    (* ********************************************************************** *)

    (* well_ord(x,r) ==> well_ord({{y,z}. y ∈ x}, Something(x,z))  **)
    lemmas well_ord_paired = paired_bij [THEN bij_is_inj, THEN well_ord_rvimage]

    lemma lepoll_trans1: "[| A \<lesssim> B; ~ A \<lesssim> C |] ==> ~ B \<lesssim> C"
    by (blast intro: lepoll_trans)

    (* ********************************************************************** *)
    (* There exists a well ordered set y such that ...                        *)
    (* ********************************************************************** *)

    lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll];

    lemma lemma2: "∃y R. well_ord(y,R) & x Int y = 0 & ~y \<lesssim> z & ~Finite(y)"
    apply (rule_tac x = "{{a,x}. a ∈ nat Un Hartog (z) }" in exI)
    apply (rule well_ord_Un [OF Ord_nat [THEN well_ord_Memrel]
                             Ord_Hartog [THEN well_ord_Memrel], THEN exE])
    apply (blast intro!: Ord_Hartog well_ord_Memrel well_ord_paired
                          lepoll_trans1 [OF _ not_Hartog_lepoll_self]
                          lepoll_trans [OF subset_imp_lepoll lepoll_paired]
           elim!: nat_not_Finite [THEN notE]
           elim: mem_asym
           dest!: Un_upper1 [THEN subset_imp_lepoll, THEN lepoll_Finite]
                  lepoll_paired [THEN lepoll_Finite])
    done

    lemma infinite_Un: "~Finite(B) ==> ~Finite(A Un B)"
    by (blast intro: subset_Finite)

    (* ********************************************************************** *)
    (* There is a v ∈ s(u) such that k \<lesssim> x Int y (in our case succ(k))    *)
    (* The idea of the proof is the following ∈                               *)
    (* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y   *)
    (* Thence y is less than or equipollent to {v ∈ Pow(x). v ≈ n#-k}      *)
    (*   We have obtained this result in two steps ∈                          *)
    (*   1. y is less than or equipollent to {v ∈ s(u). a ⊆ v}                  *)
    (*      where a is certain k-2 element subset of y                        *)
    (*   2. {v ∈ s(u). a ⊆ v} is less than or equipollent                       *)
    (*      to {v ∈ Pow(x). v ≈ n-k}                                       *)
    (* ********************************************************************** *)

    (*Proof simplified by LCP*)
    lemma succ_not_lepoll_lemma:
         "[| ~(∃x ∈ A. f`x=y); f ∈ inj(A, B); y ∈ B |]
          ==> (λa ∈ succ(A). if(a=A, y, f`a)) ∈ inj(succ(A), B)"
    apply (rule_tac d = "%z. if (z=y, A, converse (f) `z) " in lam_injective)
    apply (force simp add: inj_is_fun [THEN apply_type])
    (*this preliminary simplification prevents looping somehow*)
    apply (simp (no_asm_simp))
    apply force
    done

    lemma succ_not_lepoll_imp_eqpoll: "[| ~A ≈ B; A \<lesssim> B |] ==> succ(A) \<lesssim> B"
    apply (unfold lepoll_def eqpoll_def bij_def surj_def)
    apply (fast elim!: succ_not_lepoll_lemma inj_is_fun)
    done

    (* ********************************************************************** *)
    (* There is a k-2 element subset of y                                     *)
    (* ********************************************************************** *)

    lemmas ordertype_eqpoll =
           ordermap_bij [THEN exI [THEN eqpoll_def [THEN def_imp_iff, THEN iffD2]]]

    lemma cons_cons_subset:
         "[| a ⊆ y; b ∈ y-a; u ∈ x |] ==> cons(b, cons(u, a)) ∈ Pow(x Un y)"
    by fast

    lemma cons_cons_eqpoll:
         "[| a ≈ k; a ⊆ y; b ∈ y-a; u ∈ x; x Int y = 0 |]
          ==> cons(b, cons(u, a)) ≈ succ(succ(k))"
    by (fast intro!: cons_eqpoll_succ)

    lemma set_eq_cons:
         "[| succ(k) ≈ A; k ≈ B; B ⊆ A; a ∈ A-B; k ∈ nat |] ==> A = cons(a, B)"
    apply (rule equalityI)
    prefer 2 apply fast
    apply (rule Diff_eq_0_iff [THEN iffD1])
    apply (rule equals0I)
    apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
    apply (drule eqpoll_sym [THEN cons_eqpoll_succ], fast)
    apply (drule cons_eqpoll_succ, fast)
    apply (fast elim!: lepoll_trans [THEN lepoll_trans, THEN succ_lepoll_natE,
             OF eqpoll_sym [THEN eqpoll_imp_lepoll] subset_imp_lepoll])
    done

    lemma cons_eqE: "[| cons(x,a) = cons(y,a); x ∉ a |] ==> x = y "
    by (fast elim!: equalityE)

    lemma eq_imp_Int_eq: "A = B ==> A Int C = B Int C"
    by blast

    (* ********************************************************************** *)
    (* some arithmetic                                                        *)
    (* ********************************************************************** *)

    lemma eqpoll_sum_imp_Diff_lepoll_lemma [rule_format]:
         "[| k ∈ nat; m ∈ nat |]
          ==> ∀A B. A ≈ k #+ m & k \<lesssim> B & B ⊆ A --> A-B \<lesssim> m"
    apply (induct_tac "k")
    apply (simp add: add_0)
    apply (blast intro: eqpoll_imp_lepoll lepoll_trans
                        Diff_subset [THEN subset_imp_lepoll])
    apply (intro allI impI)
    apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], fast)
    apply (erule_tac x = "A - {xa}" in allE)
    apply (erule_tac x = "B - {xa}" in allE)
    apply (erule impE)
    apply (simp add: add_succ)
    apply (fast intro!: Diff_sing_eqpoll lepoll_Diff_sing)
    apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
    apply blast
    done

    lemma eqpoll_sum_imp_Diff_lepoll:
         "[| A ≈ succ(k #+ m); B ⊆ A; succ(k) \<lesssim> B;  k ∈ nat; m ∈ nat |]
          ==> A-B \<lesssim> m"
    apply (simp only: add_succ [symmetric])
    apply (blast intro: eqpoll_sum_imp_Diff_lepoll_lemma)
    done

    (* ********************************************************************** *)
    (* similar properties for ≈                                          *)
    (* ********************************************************************** *)

    lemma eqpoll_sum_imp_Diff_eqpoll_lemma [rule_format]:
         "[| k ∈ nat; m ∈ nat |]
          ==> ∀A B. A ≈ k #+ m & k ≈ B & B ⊆ A --> A-B ≈ m"
    apply (induct_tac "k")
    apply (force dest!: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_0_is_0])
    apply (intro allI impI)
    apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE])
    apply (fast elim!: eqpoll_imp_lepoll)
    apply (erule_tac x = "A - {xa}" in allE)
    apply (erule_tac x = "B - {xa}" in allE)
    apply (erule impE)
    apply (force intro: eqpoll_sym intro!: Diff_sing_eqpoll)
    apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
    apply blast
    done

    lemma eqpoll_sum_imp_Diff_eqpoll:
         "[| A ≈ succ(k #+ m); B ⊆ A; succ(k) ≈ B; k ∈ nat; m ∈ nat |]
          ==> A-B ≈ m"
    apply (simp only: add_succ [symmetric])
    apply (blast intro: eqpoll_sum_imp_Diff_eqpoll_lemma)
    done

    (* ********************************************************************** *)
    (* LL can be well ordered                                                 *)
    (* ********************************************************************** *)

    lemma subsets_lepoll_0_eq_unit: "{x ∈ Pow(X). x \<lesssim> 0} = {0}"
    by (fast dest!: lepoll_0_is_0 intro!: lepoll_refl)

    lemma subsets_lepoll_succ:
         "n ∈ nat ==> {z ∈ Pow(y). z \<lesssim> succ(n)} =
                      {z ∈ Pow(y). z \<lesssim> n} Un {z ∈ Pow(y). z ≈ succ(n)}"
    by (blast intro: leI le_imp_lepoll nat_into_Ord
                        lepoll_trans eqpoll_imp_lepoll
              dest!: lepoll_succ_disj)

    lemma Int_empty:
         "n ∈ nat ==> {z ∈ Pow(y). z \<lesssim> n} Int {z ∈ Pow(y). z ≈ succ(n)} = 0"
    by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
                     succ_lepoll_natE)

    locale (open) AC16 =
      fixes x and y and k and l and m and t_n and R and MM and LL and GG and s
      defines k_def:     "k   == succ(l)"
          and MM_def:    "MM  == {v ∈ t_n. succ(k) \<lesssim> v Int y}"
          and LL_def:    "LL  == {v Int y. v ∈ MM}"
          and GG_def:    "GG  == λv ∈ LL. (THE w. w ∈ MM & v ⊆ w) - v"
          and s_def:     "s(u) == {v ∈ t_n. u ∈ v & k \<lesssim> v Int y}"
      assumes all_ex:    "∀z ∈ {z ∈ Pow(x Un y) . z ≈ succ(k)}.
                           ∃! w. w ∈ t_n & z ⊆ w "
        and disjoint[iff]:  "x Int y = 0"
        and "includes":  "t_n ⊆ {v ∈ Pow(x Un y). v ≈ succ(k #+ m)}"
        and WO_R[iff]:      "well_ord(y,R)"
        and lnat[iff]:      "l ∈ nat"
        and mnat[iff]:      "m ∈ nat"
        and mpos[iff]:      "0<m"
        and Infinite[iff]:  "~ Finite(y)"
        and noLepoll:  "~ y \<lesssim> {v ∈ Pow(x). v ≈ m}"

    lemma (in AC16) knat [iff]: "k ∈ nat"
    by (simp add: k_def)

    (* ********************************************************************** *)
    (*   1. y is less than or equipollent to {v ∈ s(u). a ⊆ v}                *)
    (*      where a is certain k-2 element subset of y                        *)
    (* ********************************************************************** *)

    lemma (in AC16) Diff_Finite_eqpoll: "[| l ≈ a; a ⊆ y |] ==> y - a ≈ y"
    apply (insert WO_R Infinite lnat)
    apply (rule eqpoll_trans)
    apply (rule Diff_lesspoll_eqpoll_Card)
    apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])
    apply (blast intro: lesspoll_trans1
                intro!: Card_cardinal
                        Card_cardinal [THEN Card_is_Ord, THEN nat_le_infinite_Ord,
                                       THEN le_imp_lepoll]
                dest: well_ord_cardinal_eqpoll
                       eqpoll_sym  eqpoll_imp_lepoll
                       n_lesspoll_nat [THEN lesspoll_trans2]
                       well_ord_cardinal_eqpoll [THEN eqpoll_sym,
                              THEN eqpoll_imp_lepoll, THEN lepoll_infinite])+
    done

    lemma (in AC16) s_subset: "s(u) ⊆ t_n"
    by (unfold s_def, blast)

    lemma (in AC16) sI:
          "[| w ∈ t_n; cons(b,cons(u,a)) ⊆ w; a ⊆ y; b ∈ y-a; l ≈ a |]
           ==> w ∈ s(u)"
    apply (unfold s_def succ_def k_def)
    apply (blast intro!: eqpoll_imp_lepoll [THEN cons_lepoll_cong]
                 intro: subset_imp_lepoll lepoll_trans)
    done

    lemma (in AC16) in_s_imp_u_in: "v ∈ s(u) ==> u ∈ v"
    by (unfold s_def, blast)

    lemma (in AC16) ex1_superset_a:
         "[| l ≈ a;  a ⊆ y;  b ∈ y - a;  u ∈ x |]
          ==> ∃! c. c ∈ s(u) & a ⊆ c & b ∈ c"
    apply (rule all_ex [simplified k_def, THEN ballE])
     apply (erule ex1E)
     apply (rule_tac a = w in ex1I, blast intro: sI)
     apply (blast dest: s_subset [THEN subsetD] in_s_imp_u_in)
    apply (blast del: PowI
                 intro!: cons_cons_subset eqpoll_sym [THEN cons_cons_eqpoll])
    done

    lemma (in AC16) the_eq_cons:
         "[| ∀v ∈ s(u). succ(l) ≈ v Int y;
             l ≈ a;  a ⊆ y;  b ∈ y - a;  u ∈ x |]
          ==> (THE c. c ∈ s(u) & a ⊆ c & b ∈ c) Int y = cons(b, a)"
    apply (frule ex1_superset_a [THEN theI], assumption+)
    apply (rule set_eq_cons)
    apply (fast+)
    done

    lemma (in AC16) y_lepoll_subset_s:
         "[| ∀v ∈ s(u). succ(l) ≈ v Int y;
             l ≈ a;  a ⊆ y;  u ∈ x |]
          ==> y \<lesssim> {v ∈ s(u). a ⊆ v}"
    apply (rule Diff_Finite_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll,
                                    THEN lepoll_trans],  fast+)
    apply (rule_tac  f3 = "λb ∈ y-a. THE c. c ∈ s (u) & a ⊆ c & b ∈ c"
            in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
    apply (simp add: inj_def)
    apply (rule conjI)
    apply (rule lam_type)
    apply (frule ex1_superset_a [THEN theI], fast+, clarify)
    apply (rule cons_eqE [of _ a])
    apply (drule_tac A = "THE c. ?P (c) " and C = y in eq_imp_Int_eq)
    apply (simp_all add: the_eq_cons)
    done

    (* ********************************************************************** *)
    (* back to the second part                                                *)
    (* ********************************************************************** *)

    (*relies on the disjointness of x, y*)
    lemma (in AC16) x_imp_not_y [dest]: "a ∈ x ==> a ∉ y"
    by (blast dest:  disjoint [THEN equalityD1, THEN subsetD, OF IntI])

    lemma (in AC16) w_Int_eq_w_Diff:
         "w ⊆ x Un y ==> w Int (x - {u}) = w - cons(u, w Int y)"
    by blast

    lemma (in AC16) w_Int_eqpoll_m:
         "[| w ∈ {v ∈ s(u). a ⊆ v};
             l ≈ a;  u ∈ x;
             ∀v ∈ s(u). succ(l) ≈ v Int y |]
          ==> w Int (x - {u}) ≈ m"
    apply (erule CollectE)
    apply (subst w_Int_eq_w_Diff)
    apply (fast dest!: s_subset [THEN subsetD]
                       "includes" [simplified k_def, THEN subsetD])
    apply (blast dest: s_subset [THEN subsetD]
                       "includes" [simplified k_def, THEN subsetD]
                 dest: eqpoll_sym [THEN cons_eqpoll_succ, THEN eqpoll_sym]
                       in_s_imp_u_in
                intro!: eqpoll_sum_imp_Diff_eqpoll)
    done

    (* ********************************************************************** *)
    (*   2. {v ∈ s(u). a ⊆ v} is less than or equipollent                       *)
    (*      to {v ∈ Pow(x). v ≈ n-k}                                       *)
    (* ********************************************************************** *)

    lemma (in AC16) eqpoll_m_not_empty: "a ≈ m ==> a ≠ 0"
    apply (insert mpos)
    apply (fast elim!: zero_lt_natE dest!: eqpoll_succ_imp_not_empty)
    done

    lemma (in AC16) cons_cons_in:
         "[| z ∈ xa Int (x - {u}); l ≈ a; a ⊆ y; u ∈ x |]
          ==> ∃! w. w ∈ t_n & cons(z, cons(u, a)) ⊆ w"
    apply (rule all_ex [THEN bspec])
    apply (unfold k_def)
    apply (fast intro!: cons_eqpoll_succ elim: eqpoll_sym)
    done

    lemma (in AC16) subset_s_lepoll_w:
         "[| ∀v ∈ s(u). succ(l) ≈ v Int y; a ⊆ y; l ≈ a; u ∈ x |]
          ==> {v ∈ s(u). a ⊆ v} \<lesssim> {v ∈ Pow(x). v ≈ m}"
    apply (rule_tac f3 = "λw ∈ {v ∈ s (u) . a ⊆ v}. w Int (x - {u})"
           in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
    apply (simp add: inj_def)
    apply (intro conjI lam_type CollectI)
      apply fast
     apply (blast intro: w_Int_eqpoll_m)
    apply (intro ballI impI)
    (** LEVEL 8 **)
    apply (rule w_Int_eqpoll_m [THEN eqpoll_m_not_empty, THEN not_emptyE])
    apply (blast, assumption+)
    apply (drule equalityD1 [THEN subsetD], assumption)
    apply (frule cons_cons_in, assumption+)
    apply (blast dest: ex1_two_eq intro: s_subset [THEN subsetD] in_s_imp_u_in)+
    done

    (* ********************************************************************** *)
    (* well_ord_subsets_lepoll_n                                              *)
    (* ********************************************************************** *)

    lemma (in AC16) well_ord_subsets_eqpoll_n:
         "n ∈ nat ==> ∃S. well_ord({z ∈ Pow(y) . z ≈ succ(n)}, S)"
    apply (rule WO_R [THEN well_ord_infinite_subsets_eqpoll_X,
                      THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
    apply (fast intro: bij_is_inj [THEN well_ord_rvimage])+
    done

    lemma (in AC16) well_ord_subsets_lepoll_n:
         "n ∈ nat ==> ∃R. well_ord({z ∈ Pow(y). z \<lesssim> n}, R)"
    apply (induct_tac "n")
    apply (force intro!: well_ord_unit simp add: subsets_lepoll_0_eq_unit)
    apply (erule exE)
    apply (rule well_ord_subsets_eqpoll_n [THEN exE], assumption)
    apply (simp add: subsets_lepoll_succ)
    apply (drule well_ord_radd, assumption)
    apply (erule Int_empty [THEN disj_Un_eqpoll_sum,
                      THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
    apply (fast elim!: bij_is_inj [THEN well_ord_rvimage])
    done

    lemma (in AC16) LL_subset: "LL ⊆ {z ∈ Pow(y). z \<lesssim> succ(k #+ m)}"
    apply (unfold LL_def MM_def)
    apply (insert "includes")
    apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
    done

    lemma (in AC16) well_ord_LL: "∃S. well_ord(LL,S)"
    apply (rule well_ord_subsets_lepoll_n [THEN exE, of "succ(k#+m)"])
    apply simp
    apply (blast intro: well_ord_subset [OF _ LL_subset])
    done

    (* ********************************************************************** *)
    (* every element of LL is a contained in exactly one element of MM        *)
    (* ********************************************************************** *)

    lemma (in AC16) unique_superset_in_MM:
         "v ∈ LL ==> ∃! w. w ∈ MM & v ⊆ w"
    apply (unfold MM_def LL_def, safe, fast)
    apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
    apply (rule_tac x = x in all_ex [THEN ballE])
    apply (blast intro: eqpoll_sym)+
    done

    (* ********************************************************************** *)
    (* The function GG satisfies the conditions of WO4                        *)
    (* ********************************************************************** *)

    (* ********************************************************************** *)
    (* The union of appropriate values is the whole x                         *)
    (* ********************************************************************** *)

    lemma (in AC16) Int_in_LL: "w ∈ MM ==> w Int y ∈ LL"
    by (unfold LL_def, fast)

    lemma (in AC16) in_LL_eq_Int:
         "v ∈ LL ==> v = (THE x. x ∈ MM & v ⊆ x) Int y"
    apply (unfold LL_def, clarify)
    apply (subst unique_superset_in_MM [THEN the_equality2])
    apply (auto simp add: Int_in_LL)
    done

    lemma (in AC16) unique_superset1: "a ∈ LL ==> (THE x. x ∈ MM ∧ a ⊆ x) ∈ MM"
    by (erule unique_superset_in_MM [THEN theI, THEN conjunct1])

    lemma (in AC16) the_in_MM_subset:
         "v ∈ LL ==> (THE x. x ∈ MM & v ⊆ x) ⊆ x Un y"
    apply (drule unique_superset1)
    apply (unfold MM_def)
    apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
    done

    lemma (in AC16) GG_subset: "v ∈ LL ==> GG ` v ⊆ x"
    apply (unfold GG_def)
    apply (frule the_in_MM_subset)
    apply (frule in_LL_eq_Int)
    apply (force elim: equalityE)
    done

    lemma (in AC16) nat_lepoll_ordertype: "nat \<lesssim> ordertype(y, R)"
    apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll])
     apply (rule Ord_ordertype [OF WO_R])
    apply (rule ordertype_eqpoll [THEN eqpoll_imp_lepoll, THEN lepoll_infinite])
     apply (rule WO_R)
    apply (rule Infinite)
    done

    lemma (in AC16) ex_subset_eqpoll_n: "n ∈ nat ==> ∃z. z ⊆ y & n ≈ z"
    apply (erule nat_lepoll_imp_ex_eqpoll_n)
    apply (rule lepoll_trans [OF nat_lepoll_ordertype])
    apply (rule ordertype_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll])
    apply (rule WO_R)
    done

    lemma (in AC16) exists_proper_in_s: "u ∈ x ==> ∃v ∈ s(u). succ(k) \<lesssim> v Int y"
    apply (rule ccontr)
    apply (subgoal_tac "∀v ∈ s (u) . k ≈ v Int y")
    prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
    apply (unfold k_def)
    apply (insert all_ex "includes" lnat)
    apply (rule ex_subset_eqpoll_n [THEN exE], assumption)
    apply (rule noLepoll [THEN notE])
    apply (blast intro: lepoll_trans [OF y_lepoll_subset_s subset_s_lepoll_w])
    done

    lemma (in AC16) exists_in_MM: "u ∈ x ==> ∃w ∈ MM. u ∈ w"
    apply (erule exists_proper_in_s [THEN bexE])
    apply (unfold MM_def s_def, fast)
    done

    lemma (in AC16) exists_in_LL: "u ∈ x ==> ∃w ∈ LL. u ∈ GG`w"
    apply (rule exists_in_MM [THEN bexE], assumption)
    apply (rule bexI)
    apply (erule_tac [2] Int_in_LL)
    apply (unfold GG_def)
    apply (simp add: Int_in_LL)
    apply (subst unique_superset_in_MM [THEN the_equality2])
    apply (fast elim!: Int_in_LL)+
    done

    lemma (in AC16) OUN_eq_x: "well_ord(LL,S) ==>
          (\<Union>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x"
    apply (rule equalityI)
    apply (rule subsetI)
    apply (erule OUN_E)
    apply (rule GG_subset [THEN subsetD])
    prefer 2 apply assumption
    apply (blast intro: ltD  ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun,
                                           THEN apply_type])
    apply (rule subsetI)
    apply (erule exists_in_LL [THEN bexE])
    apply (force intro: ltI [OF _ Ord_ordertype]
                        ordermap_type [THEN apply_type]
                 simp add: ordermap_bij [THEN bij_is_inj, THEN left_inverse])
    done

    (* ********************************************************************** *)
    (* Every element of the family is less than or equipollent to n-k (m)     *)
    (* ********************************************************************** *)

    lemma (in AC16) in_MM_eqpoll_n: "w ∈ MM ==> w ≈ succ(k #+ m)"
    apply (unfold MM_def)
    apply (fast dest: "includes" [THEN subsetD])
    done

    lemma (in AC16) in_LL_eqpoll_n: "w ∈ LL ==> succ(k) \<lesssim> w"
    by (unfold LL_def MM_def, fast)

    lemma (in AC16) in_LL: "w ∈ LL ==> w ⊆ (THE x. x ∈ MM ∧ w ⊆ x)"
    by (erule subset_trans [OF in_LL_eq_Int [THEN equalityD1] Int_lower1])

    lemma (in AC16) all_in_lepoll_m:
          "well_ord(LL,S) ==>
           ∀b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) \<lesssim> m"
    apply (unfold GG_def)
    apply (rule oallI)
    apply (simp add: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN apply_type])
    apply (insert "includes")
    apply (rule eqpoll_sum_imp_Diff_lepoll)
    apply (blast del: subsetI
                 dest!: ltD
                 intro!: eqpoll_sum_imp_Diff_lepoll in_LL_eqpoll_n
                 intro: in_LL   unique_superset1 [THEN in_MM_eqpoll_n]
                        ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun,
                                      THEN apply_type])+
    done

    lemma (in AC16) conclusion:
         "∃a f. Ord(a) & domain(f) = a & (\<Union>b<a. f ` b) = x & (∀b<a. f ` b \<lesssim> m)"
    apply (rule well_ord_LL [THEN exE])
    apply (rename_tac S)
    apply (rule_tac x = "ordertype (LL,S)" in exI)
    apply (rule_tac x = "λb ∈ ordertype(LL,S).
                          GG ` (converse (ordermap (LL,S)) ` b)"  in exI)
    apply (simp add: ltD)
    apply (blast intro: lam_funtype [THEN domain_of_fun]
                        Ord_ordertype  OUN_eq_x  all_in_lepoll_m [THEN ospec])
    done

    (* ********************************************************************** *)
    (* The main theorem AC16(n, k) ==> WO4(n-k)                               *)
    (* ********************************************************************** *)

    theorem AC16_WO4:
         "[| AC16(k #+ m, k); 0 < k; 0 < m; k ∈ nat; m ∈ nat |] ==> WO4(m)"
    apply (unfold AC16_def WO4_def)
    apply (rule allI)
    apply (case_tac "Finite (A)")
    apply (rule lemma1, assumption+)
    apply (cut_tac lemma2)
    apply (elim exE conjE)
    apply (erule_tac x = "A Un y" in allE)
    apply (frule infinite_Un, drule mp, assumption)
    apply (erule zero_lt_natE, assumption, clarify)
    apply (blast intro: AC16.conclusion)
    done

    end

lemma lemma1:

      [| Finite(A); 0 < m; m ∈ nat |]
      ==> ∃a f. Ord(a) ∧
                domain(f) = a ∧ (\<Union>b<a. f ` b) = A ∧ (∀b<a. f ` b lepoll m)

lemmas well_ord_paired:

      well_ord(B, r)
      ==> well_ord
           ({{y, z2} . y ∈ B},
            rvimage({{y, z2} . y ∈ B}, λz∈{{y, z2} . y ∈ B}. THE y. {y, z2} = z, r))

lemmas well_ord_paired:

      well_ord(B, r)
      ==> well_ord
           ({{y, z2} . y ∈ B},
            rvimage({{y, z2} . y ∈ B}, λz∈{{y, z2} . y ∈ B}. THE y. {y, z2} = z, r))

lemma lepoll_trans1:

      [| A lepoll B; ¬ A lepoll C |] ==> ¬ B lepoll C

lemmas lepoll_paired:

      X lepoll {{y, z2} . y ∈ X}

lemmas lepoll_paired:

      X lepoll {{y, z2} . y ∈ X}

lemma lemma2:

      ∃y R. well_ord(y, R) ∧ x ∩ y = 0 ∧ ¬ y lepoll z ∧ ¬ Finite(y)

lemma infinite_Un:

      ¬ Finite(B) ==> ¬ Finite(A ∪ B)

lemma succ_not_lepoll_lemma:

      [| ¬ (∃x∈A. f ` x = y); f ∈ inj(A, B); y ∈ B |]
      ==> (λa∈succ(A). if a = A then y else f ` a) ∈ inj(succ(A), B)

lemma succ_not_lepoll_imp_eqpoll:

      [| ¬ A ≈ B; A lepoll B |] ==> succ(A) lepoll B

lemmas ordertype_eqpoll:

      well_ord(A2, r4) ==> A2 ≈ ordertype(A2, r4)

lemmas ordertype_eqpoll:

      well_ord(A2, r4) ==> A2 ≈ ordertype(A2, r4)

lemma cons_cons_subset:

      [| a ⊆ y; b ∈ y - a; u ∈ x |] ==> cons(b, cons(u, a)) ∈ Pow(x ∪ y)

lemma cons_cons_eqpoll:

      [| a ≈ k; a ⊆ y; b ∈ y - a; u ∈ x; x ∩ y = 0 |]
      ==> cons(b, cons(u, a)) ≈ succ(succ(k))

lemma set_eq_cons:

      [| succ(k) ≈ A; k ≈ B; B ⊆ A; a ∈ A - B; k ∈ nat |] ==> A = cons(a, B)

lemma cons_eqE:

      [| cons(x, a) = cons(y, a); x ∉ a |] ==> x = y

lemma eq_imp_Int_eq:

      A = B ==> A ∩ C = B ∩ C

lemma eqpoll_sum_imp_Diff_lepoll_lemma:

      [| k ∈ nat; m ∈ nat; A ≈ k #+ m ∧ k lepoll B ∧ B ⊆ A |] ==> A - B lepoll m

lemma eqpoll_sum_imp_Diff_lepoll:

      [| A ≈ succ(k #+ m); B ⊆ A; succ(k) lepoll B; k ∈ nat; m ∈ nat |]
      ==> A - B lepoll m

lemma eqpoll_sum_imp_Diff_eqpoll_lemma:

      [| k ∈ nat; m ∈ nat; A ≈ k #+ m ∧ k ≈ B ∧ B ⊆ A |] ==> A - B ≈ m

lemma eqpoll_sum_imp_Diff_eqpoll:

      [| A ≈ succ(k #+ m); B ⊆ A; succ(k) ≈ B; k ∈ nat; m ∈ nat |] ==> A - B ≈ m

lemma subsets_lepoll_0_eq_unit:

      {x ∈ Pow(X) . x lepoll 0} = {0}

lemma subsets_lepoll_succ:

      n ∈ nat
      ==> {z ∈ Pow(y) . z lepoll succ(n)} =
          {z ∈ Pow(y) . z lepoll n} ∪ {z ∈ Pow(y) . z ≈ succ(n)}

lemma Int_empty:

      n ∈ nat ==> {z ∈ Pow(y) . z lepoll n} ∩ {z ∈ Pow(y) . z ≈ succ(n)} = 0

lemma knat:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m} |]
      ==> succ(l) ∈ nat

lemma Diff_Finite_eqpoll:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; l ≈ a; a ⊆ y |]
      ==> y - a ≈ y

lemma s_subset:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m} |]
      ==> {v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y} ⊆ t_n

lemma sI:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; w ∈ t_n;
         cons(b, cons(u, a)) ⊆ w; a ⊆ y; b ∈ y - a; l ≈ a |]
      ==> w ∈ {v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y}

lemma in_s_imp_u_in:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         v ∈ {v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y} |]
      ==> u ∈ v

lemma ex1_superset_a:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; l ≈ a; a ⊆ y;
         b ∈ y - a; u ∈ x |]
      ==> ∃!c. c ∈ {v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y} ∧ a ⊆ c ∧ b ∈ c

lemma the_eq_cons:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         ∀v∈{v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y}. succ(l) ≈ v ∩ y; l ≈ a; a ⊆ y;
         b ∈ y - a; u ∈ x |]
      ==> (THE c. c ∈ {v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y} ∧ a ⊆ c ∧ b ∈ c) ∩ y =
          cons(b, a)

lemma y_lepoll_subset_s:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         ∀v∈{v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y}. succ(l) ≈ v ∩ y; l ≈ a; a ⊆ y;
         u ∈ x |]
      ==> y lepoll {v ∈ {v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y} . a ⊆ v}

lemma x_imp_not_y:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; a ∈ x |]
      ==> a ∉ y

lemma w_Int_eq_w_Diff:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; w ⊆ x ∪ y |]
      ==> w ∩ (x - {u}) = w - cons(u, w ∩ y)

lemma w_Int_eqpoll_m:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         w ∈ {v ∈ {v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y} . a ⊆ v}; l ≈ a; u ∈ x;
         ∀v∈{v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y}. succ(l) ≈ v ∩ y |]
      ==> w ∩ (x - {u}) ≈ m

lemma eqpoll_m_not_empty:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; a ≈ m |]
      ==> a ≠ 0

lemma cons_cons_in:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         z ∈ xa ∩ (x - {u}); l ≈ a; a ⊆ y; u ∈ x |]
      ==> ∃!w. w ∈ t_n ∧ cons(z, cons(u, a)) ⊆ w

lemma subset_s_lepoll_w:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         ∀v∈{v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y}. succ(l) ≈ v ∩ y; a ⊆ y; l ≈ a;
         u ∈ x |]
      ==> {v ∈ {v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y} . a ⊆ v} lepoll
          {v ∈ Pow(x) . v ≈ m}

lemma well_ord_subsets_eqpoll_n:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; n ∈ nat |]
      ==> ∃S. well_ord({z ∈ Pow(y) . z ≈ succ(n)}, S)

lemma well_ord_subsets_lepoll_n:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; n ∈ nat |]
      ==> ∃R. well_ord({z ∈ Pow(y) . z lepoll n}, R)

lemma LL_subset:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m} |]
      ==> {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}} ⊆
          {z ∈ Pow(y) . z lepoll succ(succ(l) #+ m)}

lemma well_ord_LL:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m} |]
      ==> ∃S. well_ord({v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}, S)

lemma unique_superset_in_MM:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         v ∈ {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}} |]
      ==> ∃!w. w ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ v ⊆ w

lemma Int_in_LL:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         w ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} |]
      ==> w ∩ y ∈ {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}

lemma in_LL_eq_Int:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         v ∈ {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}} |]
      ==> v = (THE x. x ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ v ⊆ x) ∩ y

lemma unique_superset1:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         a ∈ {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}} |]
      ==> (THE x. x ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ a ⊆ x) ∈
          {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}

lemma the_in_MM_subset:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         v ∈ {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}} |]
      ==> (THE x. x ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ v ⊆ x) ⊆ x ∪ y

lemma GG_subset:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         v ∈ {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}} |]
      ==> (λv∈{v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}.
              (THE w. w ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ v ⊆ w) - v) `
          v ⊆
          x

lemma nat_lepoll_ordertype:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m} |]
      ==> nat lepoll ordertype(y, R)

lemma ex_subset_eqpoll_n:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; n ∈ nat |]
      ==> ∃z. z ⊆ y ∧ n ≈ z

lemma exists_proper_in_s:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; u ∈ x |]
      ==> ∃v∈{v ∈ t_n . u ∈ v ∧ succ(l) lepoll v ∩ y}. succ(succ(l)) lepoll v ∩ y

lemma exists_in_MM:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; u ∈ x |]
      ==> ∃w∈{v ∈ t_n . succ(succ(l)) lepoll v ∩ y}. u ∈ w

lemma exists_in_LL:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m}; u ∈ x |]
      ==> ∃w∈{v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}.
             u ∈ (λv∈{v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}.
                     (THE w. w ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ v ⊆ w) -
                     v) `
                 w

lemma OUN_eq_x:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         well_ord({v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}, S) |]
      ==> (\<Union>b<ordertype
                      ({v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}, S).
              (λv∈{v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}.
                  (THE w. w ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ v ⊆ w) - v) `
              (converse
                (ordermap({v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}, S)) `
               b)) =
          x

lemma in_MM_eqpoll_n:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         w ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} |]
      ==> w ≈ succ(succ(l) #+ m)

lemma in_LL_eqpoll_n:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         w ∈ {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}} |]
      ==> succ(succ(l)) lepoll w

lemma in_LL:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         w ∈ {v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}} |]
      ==> w ⊆ (THE x. x ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ w ⊆ x)

lemma all_in_lepoll_m:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m};
         well_ord({v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}, S) |]
      ==> ∀b<ordertype({v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}, S).
             (λv∈{v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}.
                 (THE w. w ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y} ∧ v ⊆ w) - v) `
             (converse
               (ordermap({v ∩ y . v ∈ {v ∈ t_n . succ(succ(l)) lepoll v ∩ y}}, S)) `
              b) lepoll
             m

lemma conclusion:

      [| ∀z∈{z ∈ Pow(x ∪ y) . z ≈ succ(succ(l))}. ∃!w. w ∈ t_n ∧ z ⊆ w; x ∩ y = 0;
         t_n ⊆ {v ∈ Pow(x ∪ y) . v ≈ succ(succ(l) #+ m)}; well_ord(y, R); l ∈ nat;
         m ∈ nat; 0 < m; ¬ Finite(y); ¬ y lepoll {v ∈ Pow(x) . v ≈ m} |]
      ==> ∃a f. Ord(a) ∧
                domain(f) = a ∧ (\<Union>b<a. f ` b) = x ∧ (∀b<a. f ` b lepoll m)

theorem AC16_WO4:

      [| AC16(k #+ m, k); 0 < k; 0 < m; k ∈ nat; m ∈ nat |] ==> WO4(m)