section‹The Axiom of Extensionality in $M[G]$›
theory Extensionality_Axiom
imports
Names
begin
context forcing_data
begin
lemma extensionality_in_MG : "extensionality(##(M[G]))"
proof -
{
fix x y z
assume
asms: "x∈M[G]" "y∈M[G]" "(∀w∈M[G] . w ∈ x ⟷ w ∈ y)"
from ‹x∈M[G]› have
"z∈x ⟷ z∈M[G] ∧ z∈x"
using transitivity_MG by auto
also have
"... ⟷ z∈y"
using asms transitivity_MG by auto
finally have
"z∈x ⟷ z∈y" .
}
then have
"∀x∈M[G] . ∀y∈M[G] . (∀z∈M[G] . z ∈ x ⟷ z ∈ y) ⟶ x = y"
by blast
then show ?thesis unfolding extensionality_def by simp
qed
end
end