Theory Extensionality_Axiom
section‹The Axiom of Extensionality in $M[G]$›
theory Extensionality_Axiom
imports
Names
begin
context forcing_data1
begin
lemma extensionality_in_MG : "extensionality(##(M[G]))"
unfolding extensionality_def
proof(clarsimp)
fix x y
assume "x∈M[G]" "y∈M[G]" "(∀w∈M[G] . w ∈ x ⟷ w ∈ y)"
moreover from this
have "z∈x ⟷ z∈M[G] ∧ z∈y" for z
using transitivity_MG by auto
moreover from calculation
have "z∈M[G] ∧ z∈x ⟷ z∈y" for z
using transitivity_MG by auto
ultimately
show "x=y"
by auto
qed
end
end