# Theory Foundation_Axiom

section‹The Axiom of Foundation in $M[G]$›
theory Foundation_Axiom
imports
Names
begin
context forcing_data1
begin
lemma foundation_in_MG : "foundation_ax(##(M[G]))"
unfolding foundation_ax_def
by (rule rallI, cut_tac A=x in foundation, auto intro: transitivity_MG)
lemma "foundation_ax(##(M[G]))"
proof -
{
fix x
assume "x∈M[G]" "∃y∈M[G] . y∈x"
then
have "∃y∈M[G] . y∈x∩M[G]"
by simp
then
obtain y where "y∈x∩M[G]" "∀z∈y. z ∉ x∩M[G]"
using foundation[of "x∩M[G]"] by blast
then
have "∃y∈M[G] . y ∈ x ∧ (∀z∈M[G] . z ∉ x ∨ z ∉ y)"
by auto
}
then
show ?thesis
unfolding foundation_ax_def by auto
qed
end
end