section‹The Axiom of Pairing in $M[G]$›
theory Pairing_Axiom imports Names begin
context forcing_data
begin
lemma val_Upair :
"one ∈ G ⟹ val(P,G,{⟨τ,one⟩,⟨ρ,one⟩}) = {val(P,G,τ),val(P,G,ρ)}"
by (insert one_in_P, rule trans, subst def_val,auto simp add: Sep_and_Replace)
lemma pairing_in_MG :
assumes "M_generic(G)"
shows "upair_ax(##M[G])"
proof -
{
fix x y
have "one∈G" using assms one_in_G by simp
from assms
have "G⊆P" unfolding M_generic_def and filter_def by simp
with ‹one∈G›
have "one∈P" using subsetD by simp
then
have "one∈M" using transitivity[OF _ P_in_M] by simp
assume "x ∈ M[G]" "y ∈ M[G]"
then
obtain τ ρ where
0 : "val(P,G,τ) = x" "val(P,G,ρ) = y" "ρ ∈ M" "τ ∈ M"
using GenExtD by blast
with ‹one∈M›
have "⟨τ,one⟩ ∈ M" "⟨ρ,one⟩∈M" using pair_in_M_iff by auto
then
have 1: "{⟨τ,one⟩,⟨ρ,one⟩} ∈ M" (is "?σ ∈ _") using upair_in_M_iff by simp
then
have "val(P,G,?σ) ∈ M[G]" using GenExtI by simp
with 1
have "{val(P,G,τ),val(P,G,ρ)} ∈ M[G]" using val_Upair assms one_in_G by simp
with 0
have "{x,y} ∈ M[G]" by simp
}
then show ?thesis unfolding upair_ax_def upair_def by auto
qed
end
end