section‹The Axiom of Choice in $M[G]$› theory Choice_Axiom imports Powerset_Axiom Extensionality_Axiom Foundation_Axiom Replacement_Axiom Infinity_Axiom begin definition upair_name :: "i ⇒ i ⇒ i ⇒ i" where "upair_name(τ,ρ,on) ≡ Upair(⟨τ,on⟩,⟨ρ,on⟩)" definition opair_name :: "i ⇒ i ⇒ i ⇒ i" where "opair_name(τ,ρ,on) ≡ upair_name(upair_name(τ,τ,on),upair_name(τ,ρ,on),on)" definition induced_surj :: "i⇒i⇒i⇒i" where "induced_surj(f,a,e) ≡ f-``(range(f)-a)×{e} ∪ restrict(f,f-``a)" lemma domain_induced_surj: "domain(induced_surj(f,a,e)) = domain(f)" unfolding induced_surj_def using domain_restrict domain_of_prod by auto lemma range_restrict_vimage: assumes "function(f)" shows "range(restrict(f,f-``a)) ⊆ a" proof from assms have "function(restrict(f,f-``a))" using function_restrictI by simp fix y assume "y ∈ range(restrict(f,f-``a))" then obtain x where "⟨x,y⟩ ∈ restrict(f,f-``a)" "x ∈ f-``a" "x∈domain(f)" using domain_restrict domainI[of _ _ "restrict(f,f-``a)"] by auto moreover note ‹function(restrict(f,f-``a))› ultimately have "y = restrict(f,f-``a)`x" using function_apply_equality by blast also from ‹x ∈ f-``a› have "restrict(f,f-``a)`x = f`x" by simp finally have "y = f`x" . moreover from assms ‹x∈domain(f)› have "⟨x,f`x⟩ ∈ f" using function_apply_Pair by auto moreover note assms ‹x ∈ f-``a› ultimately show "y∈a" using function_image_vimage[of f a] by auto qed lemma induced_surj_type: assumes "function(f)" (* "relation(f)" (* a function can contain non-pairs *) *) shows "induced_surj(f,a,e): domain(f) → {e} ∪ a" and "x ∈ f-``a ⟹ induced_surj(f,a,e)`x = f`x" proof - let ?f1="f-``(range(f)-a) × {e}" and ?f2="restrict(f, f-``a)" have "domain(?f2) = domain(f) ∩ f-``a" using domain_restrict by simp moreover from assms have "domain(?f1) = f-``(range(f))-f-``a" using domain_of_prod function_vimage_Diff by simp ultimately have "domain(?f1) ∩ domain(?f2) = 0" by auto moreover have "function(?f1)" "relation(?f1)" "range(?f1) ⊆ {e}" unfolding function_def relation_def range_def by auto moreover from this and assms have "?f1: domain(?f1) → range(?f1)" using function_imp_Pi by simp moreover from assms have "?f2: domain(?f2) → range(?f2)" using function_imp_Pi[of "restrict(f, f -`` a)"] function_restrictI by simp moreover from assms have "range(?f2) ⊆ a" using range_restrict_vimage by simp ultimately have "induced_surj(f,a,e): domain(?f1) ∪ domain(?f2) → {e} ∪ a" unfolding induced_surj_def using fun_is_function fun_disjoint_Un fun_weaken_type by simp moreover have "domain(?f1) ∪ domain(?f2) = domain(f)" using domain_restrict domain_of_prod by auto ultimately show "induced_surj(f,a,e): domain(f) → {e} ∪ a" by simp assume "x ∈ f-``a" then have "?f2`x = f`x" using restrict by simp moreover from ‹x ∈ f-``a› ‹domain(?f1) = _› have "x ∉ domain(?f1)" by simp ultimately show "induced_surj(f,a,e)`x = f`x" unfolding induced_surj_def using fun_disjoint_apply2[of x ?f1 ?f2] by simp qed lemma induced_surj_is_surj : assumes "e∈a" "function(f)" "domain(f) = α" "⋀y. y ∈ a ⟹ ∃x∈α. f ` x = y" shows "induced_surj(f,a,e) ∈ surj(α,a)" unfolding surj_def proof (intro CollectI ballI) from assms show "induced_surj(f,a,e): α → a" using induced_surj_type[of f a e] cons_eq cons_absorb by simp fix y assume "y ∈ a" with assms have "∃x∈α. f ` x = y" by simp then obtain x where "x∈α" "f ` x = y" by auto with ‹y∈a› assms have "x∈f-``a" using vimage_iff function_apply_Pair[of f x] by auto with ‹f ` x = y› assms have "induced_surj(f, a, e) ` x = y" using induced_surj_type by simp with ‹x∈α› show "∃x∈α. induced_surj(f, a, e) ` x = y" by auto qed lemma (in M_ZF1_trans) upair_name_closed : "⟦ x∈M; y∈M ; o∈M⟧ ⟹ upair_name(x,y,o)∈M" unfolding upair_name_def using upair_in_M_iff pair_in_M_iff Upair_eq_cons by simp context G_generic1 begin lemma val_upair_name : "val(G,upair_name(τ,ρ,𝟭)) = {val(G,τ),val(G,ρ)}" unfolding upair_name_def using val_Upair Upair_eq_cons generic one_in_G by simp lemma val_opair_name : "val(G,opair_name(τ,ρ,𝟭)) = ⟨val(G,τ),val(G,ρ)⟩" unfolding opair_name_def Pair_def using val_upair_name by simp lemma val_RepFun_one: "val(G,{⟨f(x),𝟭⟩ . x∈a}) = {val(G,f(x)) . x∈a}" proof - let ?A = "{f(x) . x ∈ a}" let ?Q = "λ⟨x,p⟩ . p = 𝟭" have "𝟭 ∈ ℙ∩G" using generic one_in_G one_in_P by simp have "{⟨f(x),𝟭⟩ . x ∈ a} = {t ∈ ?A × ℙ . ?Q(t)}" using one_in_P by force then have "val(G,{⟨f(x),𝟭⟩ . x ∈ a}) = val(G,{t ∈ ?A × ℙ . ?Q(t)})" by simp also have "... = {z . t ∈ ?A , (∃p∈ℙ∩G . ?Q(⟨t,p⟩)) ∧ z= val(G,t)}" using val_of_name_alt by simp also from ‹𝟭∈ℙ∩G› have "... = {val(G,t) . t ∈ ?A }" by force also have "... = {val(G,f(x)) . x ∈ a}" by auto finally show ?thesis by simp qed end― ‹\<^locale>‹G_generic1›› subsection‹$M[G]$ is a transitive model of ZF› sublocale G_generic1 ⊆ ext:M_Z_trans "M[G]" using Transset_MG generic pairing_in_MG Union_MG extensionality_in_MG power_in_MG foundation_in_MG replacement_assm_MG separation_in_MG infinity_in_MG replacement_ax1 by unfold_locales lemma (in M_replacement) upair_name_lam_replacement : "M(z) ⟹ lam_replacement(M,λx . upair_name(fst(x),snd(x),z))" using lam_replacement_Upair[THEN [5] lam_replacement_hcomp2] lam_replacement_product lam_replacement_fst lam_replacement_snd lam_replacement_constant unfolding upair_name_def by simp lemma (in forcing_data1) repl_opname_check : assumes "A∈M" "f∈M" shows "{opair_name(check(x),f`x,𝟭). x∈A}∈M" using assms lam_replacement_constant check_lam_replacement lam_replacement_identity upair_name_lam_replacement[THEN [5] lam_replacement_hcomp2] lam_replacement_apply2[THEN [5] lam_replacement_hcomp2] lam_replacement_imp_strong_replacement_aux transitivity RepFun_closed upair_name_closed apply_closed unfolding opair_name_def by simp theorem (in G_generic1) choice_in_MG: assumes "choice_ax(##M)" shows "choice_ax(##M[G])" proof - { fix a assume "a∈M[G]" then obtain τ where "τ∈M" "val(G,τ) = a" using GenExt_def by auto with ‹τ∈M› have "domain(τ)∈M" using domain_closed by simp then obtain s α where "s∈surj(α,domain(τ))" "Ord(α)" "s∈M" "α∈M" using assms choice_ax_abs by auto then have "α∈M[G]" using M_subset_MG generic one_in_G subsetD by blast let ?A="domain(τ)×ℙ" let ?g = "{opair_name(check(β),s`β,𝟭). β∈α}" have "?g ∈ M" using ‹s∈M› ‹α∈M› repl_opname_check by simp let ?f_dot="{⟨opair_name(check(β),s`β,𝟭),𝟭⟩. β∈α}" have "?f_dot = ?g × {𝟭}" by blast define f where "f ≡ val(G,?f_dot)" from ‹?g∈M› ‹?f_dot = ?g×{𝟭}› have "?f_dot∈M" using cartprod_closed singleton_closed by simp then have "f ∈ M[G]" unfolding f_def by (blast intro:GenExtI) have "f = {val(G,opair_name(check(β),s`β,𝟭)) . β∈α}" unfolding f_def using val_RepFun_one by simp also have "... = {⟨β,val(G,s`β)⟩ . β∈α}" using val_opair_name val_check generic one_in_G one_in_P by simp finally have "f = {⟨β,val(G,s`β)⟩ . β∈α}" . then have 1: "domain(f) = α" "function(f)" unfolding function_def by auto have 2: "y ∈ a ⟹ ∃x∈α. f ` x = y" for y proof - fix y assume "y ∈ a" with ‹val(G,τ) = a› obtain σ where "σ∈domain(τ)" "val(G,σ) = y" using elem_of_val[of y _ τ] by blast with ‹s∈surj(α,domain(τ))› obtain β where "β∈α" "s`β = σ" unfolding surj_def by auto with ‹val(G,σ) = y› have "val(G,s`β) = y" by simp with ‹f = {⟨β,val(G,s`β)⟩ . β∈α}› ‹β∈α› have "⟨β,y⟩∈f" by auto with ‹function(f)› have "f`β = y" using function_apply_equality by simp with ‹β∈α› show "∃β∈α. f ` β = y" by auto qed then have "∃α∈(M[G]). ∃f'∈(M[G]). Ord(α) ∧ f' ∈ surj(α,a)" proof (cases "a=0") case True then show ?thesis unfolding surj_def using zero_in_MG by auto next case False with ‹a∈M[G]› obtain e where "e∈a" "e∈M[G]" using transitivity_MG by blast with 1 and 2 have "induced_surj(f,a,e) ∈ surj(α,a)" using induced_surj_is_surj by simp moreover from ‹f∈M[G]› ‹a∈M[G]› ‹e∈M[G]› have "induced_surj(f,a,e) ∈ M[G]" unfolding induced_surj_def by (simp flip: setclass_iff) moreover note ‹α∈M[G]› ‹Ord(α)› ultimately show ?thesis by auto qed } then show ?thesis using ext.choice_ax_abs by simp qed sublocale G_generic1_AC ⊆ ext:M_ZC_basic "M[G]" using choice_ax choice_in_MG by unfold_locales end