Theory Choice_Axiom

sectionThe 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 :: "iiii" 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" "xdomain(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 xdomain(f)
  have "x,f`x  f"
    using function_apply_Pair by auto
  moreover
  note assms x  f-``a
  ultimately
  show "ya"
    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
    "ea" "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 ya assms
  have "xf-``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 :
  " xM; yM ; oM  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),𝟭 . xa}) = {val(G,f(x)) . xa}"
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 , (pG . ?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― ‹localeG_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 "AM" "fM"
  shows "{opair_name(check(x),f`x,𝟭). xA}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 "aM[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 "ssurj(α,domain(τ))" "Ord(α)" "sM" "α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 sM α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 ?gM ?f_dot = ?g×{𝟭}
    have "?f_dotM"
      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 ssurj(α,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 "β,yf"
        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 aM[G]
      obtain e where "ea" "eM[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 fM[G] aM[G] eM[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