Theory Union_Axiom
section‹The Axiom of Unions in $M[G]$›
theory Union_Axiom
imports Names
begin
definition Union_name_body :: "[i,i,i,i] ⇒ o" where
"Union_name_body(P,leq,τ,x) ≡ ∃ σ∈domain(τ) . ∃q∈P . ∃r∈P .
⟨σ,q⟩ ∈ τ ∧ ⟨fst(x),r⟩ ∈ σ ∧ ⟨snd(x),r⟩ ∈ leq ∧ ⟨snd(x),q⟩ ∈ leq"
definition Union_name :: "[i,i,i] ⇒ i" where
"Union_name(P,leq,τ) ≡ {u ∈ domain(⋃(domain(τ))) × P . Union_name_body(P,leq,τ,u)}"
context forcing_data1
begin
lemma Union_name_closed :
assumes "τ ∈ M"
shows "Union_name(ℙ,leq,τ) ∈ M"
proof -
let ?Q="Union_name_body(ℙ,leq,τ)"
note lr_fst2 = lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst]
and lr_fst3 = lam_replacement_hcomp[OF lr_fst2] lam_replacement_hcomp[OF lr_fst2 lr_fst2]
note ‹τ∈M›
moreover from this
have "domain(⋃(domain(τ)))∈M" (is "?d ∈ _")
using domain_closed Union_closed by simp
moreover from this
have "?d × ℙ ∈ M"
using cartprod_closed by simp
note types = assms ‹?d×ℙ ∈ M› ‹?d∈M›
ultimately
show ?thesis
using domain_closed pair_in_M_iff fst_closed snd_closed separation_closed
lam_replacement_constant lam_replacement_hcomp
lam_replacement_fst lam_replacement_snd lam_replacement_product
separation_bex separation_conj separation_in lr_fst2 lr_fst3
lam_replacement_hcomp[OF lr_fst3(1) lam_replacement_snd]
unfolding Union_name_body_def Union_name_def
by simp
qed
lemma Union_MG_Eq :
assumes "a ∈ M[G]" and "a = val(G,τ)" and "filter(G)" and "τ ∈ M"
shows "⋃ a = val(G,Union_name(ℙ,leq,τ))"
proof (intro equalityI subsetI)
fix x
assume "x ∈ ⋃ a"
with ‹a=_›
have "x ∈ ⋃ (val(G,τ))"
by simp
then
obtain i where "i ∈ val(G,τ)" "x ∈ i"
by blast
with ‹τ ∈ M›
obtain σ q where "q ∈ G" "⟨σ,q⟩ ∈ τ" "val(G,σ) = i" "σ ∈ M"
using elem_of_val_pair domain_trans[OF trans_M] by blast
moreover from this ‹x ∈ i›
obtain θ r where "r ∈ G" "⟨θ,r⟩ ∈ σ" "val(G,θ) = x" "θ ∈ M"
using elem_of_val_pair domain_trans[OF trans_M] by blast
moreover from calculation
have "θ ∈ domain(⋃(domain(τ)))"
by auto
moreover from calculation ‹filter(G)›
obtain p where "p ∈ G" "⟨p,r⟩ ∈ leq" "⟨p,q⟩ ∈ leq" "p ∈ ℙ" "r ∈ ℙ" "q ∈ ℙ"
using low_bound_filter filterD by blast
moreover from this
have "p ∈ M" "q∈M" "r∈M"
by (auto dest:transitivity)
moreover from calculation
have "⟨θ,p⟩ ∈ Union_name(ℙ,leq,τ)"
unfolding Union_name_def Union_name_body_def
by auto
moreover from this ‹p∈ℙ› ‹p∈G›
have "val(G,θ) ∈ val(G,Union_name(ℙ,leq,τ))"
using val_of_elem by simp
ultimately
show "x ∈ val(G,Union_name(ℙ,leq,τ))"
by simp
next
fix x
assume "x ∈ (val(G,Union_name(ℙ,leq,τ)))"
moreover
note ‹filter(G)› ‹a=val(G,τ)›
moreover from calculation
obtain θ p where "p ∈ G" "⟨θ,p⟩ ∈ Union_name(ℙ,leq,τ)" "val(G,θ) = x"
using elem_of_val_pair by blast
moreover from calculation
have "p∈ℙ"
using filterD by simp
moreover from calculation
obtain σ q r where "⟨σ,q⟩ ∈ τ" "⟨θ,r⟩ ∈ σ" "⟨p,r⟩ ∈ leq" "⟨p,q⟩ ∈ leq" "r∈ℙ" "q∈ℙ"
unfolding Union_name_def Union_name_body_def
by auto
moreover from calculation
have "r ∈ G" "q ∈ G"
using filter_leqD by auto
moreover from this ‹⟨θ,r⟩ ∈ σ› ‹⟨σ,q⟩∈τ› ‹q∈ℙ› ‹r∈ℙ›
have "val(G,σ) ∈ val(G,τ)" "val(G,θ) ∈ val(G,σ)"
using val_of_elem by simp+
ultimately
show "x ∈ ⋃ a"
by blast
qed
lemma union_in_MG :
assumes "filter(G)"
shows "Union_ax(##M[G])"
unfolding Union_ax_def
proof(clarsimp)
fix a
assume "a ∈ M[G]"
moreover
note ‹filter(G)›
moreover from calculation
interpret mgtrans : M_trans "##M[G]"
using transitivity_MG by (unfold_locales; auto)
from calculation
obtain τ where "τ ∈ M" "a=val(G,τ)"
using GenExtD by blast
moreover from this
have "val(G,Union_name(ℙ,leq,τ)) ∈ M[G]"
using GenExtI Union_name_closed by simp
ultimately
show "∃z∈M[G] . big_union(##M[G],a,z)"
using Union_MG_Eq by auto
qed
theorem Union_MG : "M_generic(G) ⟹ Union_ax(##M[G])"
by (auto simp:union_in_MG)
end
end