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 (* G_generic' *) end