# 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 :: "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