section‹The Axiom of Infinity in $M[G]$›
theory Infinity_Axiom
imports Pairing_Axiom Union_Axiom Separation_Axiom
begin
context G_generic begin
interpretation mg_triv: M_trivial"##M[G]"
using transitivity_MG zero_in_MG generic Union_MG pairing_in_MG
by unfold_locales auto
lemma infinity_in_MG : "infinity_ax(##M[G])"
proof -
from infinity_ax obtain I where
Eq1: "I∈M" "0 ∈ I" "∀y∈M. y ∈ I ⟶ succ(y) ∈ I"
unfolding infinity_ax_def by auto
then have
"check(I) ∈ M"
using check_in_M by simp
then have
"I∈ M[G]"
using valcheck generic one_in_G one_in_P GenExtI[of "check(I)" G] by simp
with ‹0∈I› have "0∈M[G]" using transitivity_MG by simp
with ‹I∈M› have "y ∈ M" if "y ∈ I" for y
using transitivity[OF _ ‹I∈M›] that by simp
with ‹I∈M[G]› have "succ(y) ∈ I ∩ M[G]" if "y ∈ I" for y
using that Eq1 transitivity_MG by blast
with Eq1 ‹I∈M[G]› ‹0∈M[G]› show ?thesis
unfolding infinity_ax_def by auto
qed
end
end