Theory Pairing_Axiom
section‹The Axiom of Pairing in $M[G]$›
theory Pairing_Axiom
imports
Names
begin
context G_generic1
begin
lemma val_Upair :
"𝟭 ∈ G ⟹ val(G,{⟨τ,𝟭⟩,⟨ρ,𝟭⟩}) = {val(G,τ),val(G,ρ)}"
by (rule trans, subst def_val,auto)
lemma pairing_in_MG : "upair_ax(##M[G])"
proof -
{
fix x y
assume "x ∈ M[G]" "y ∈ M[G]"
moreover from this
obtain τ ρ where "val(G,τ) = x" "val(G,ρ) = y" "ρ ∈ M" "τ ∈ M"
using GenExtD by blast
moreover from this
have "⟨τ,𝟭⟩ ∈ M" "⟨ρ,𝟭⟩∈M"
using pair_in_M_iff by auto
moreover from this
have "{⟨τ,𝟭⟩,⟨ρ,𝟭⟩} ∈ M" (is "?σ ∈ _")
using upair_in_M_iff by simp
moreover from this
have "val(G,?σ) ∈ M[G]"
using GenExtI by simp
moreover from calculation
have "{val(G,τ),val(G,ρ)} ∈ M[G]"
using val_Upair one_in_G by simp
ultimately
have "{x,y} ∈ M[G]"
by simp
}
then
show ?thesis
unfolding upair_ax_def upair_def by auto
qed
end
end