(* 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)