Theory Choice_Axiom
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)"
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
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