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 ― ‹\<^locale>‹forcing_data1›› end