[STATEMENT]
lemma Limit_vifunion_in_Vset_if_VLambda_in_VsetI:
  assumes "Limit \<alpha>" and "VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<R>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: vrange_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<lambda>i\<in>\<^sub>\<circ>I. A i) `\<^sub>\<circ> I \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VLambda I A `\<^sub>\<circ> I \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: vimage_VLambda_vrange_rep)
[PROOF STATE]
proof (state)
this:
VLambda I A `\<^sub>\<circ> I \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
VLambda I A `\<^sub>\<circ> I \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "(\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
VLambda I A `\<^sub>\<circ> I \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vproduct_in_VsetI:
  assumes "Limit \<alpha>"
    and "I \<in>\<^sub>\<circ> Vset \<alpha>"
    and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> A i \<in>\<^sub>\<circ> Vset \<alpha>"
    and "vfinite I"
  shows "(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule Limit_vifunion_in_VsetI) (simp_all add: assms(1,3,4))
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
I \<in>\<^sub>\<circ> Vset \<alpha>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> A ?i \<in>\<^sub>\<circ> Vset \<alpha>
vfinite I
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "I \<times>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
I \<in>\<^sub>\<circ> Vset \<alpha>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> A ?i \<in>\<^sub>\<circ> Vset \<alpha>
vfinite I
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "VPow (I \<times>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i)) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VPow (I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VPow (I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from vsubset_in_VsetI[OF vproduct_vsubset_VPow[of I A] this]
[PROOF STATE]
proof (chain)
picking this:
vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vproduct_in_Vset_if_VLambda_in_VsetI:
  assumes "Limit \<alpha>" and "VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule Limit_vifunion_in_Vset_if_VLambda_in_VsetI)
      (simp_all add: assms)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "I \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. I \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (metis vdomain_VLambda vdomain_in_VsetI)
[PROOF STATE]
proof (state)
this:
I \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
I \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "I \<times>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
I \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
I \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "VPow (I \<times>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i)) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VPow (I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VPow (I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from vsubset_in_VsetI[OF vproduct_vsubset_VPow[of I A] this]
[PROOF STATE]
proof (chain)
picking this:
vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vproduct I A \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vdunion_in_Vset_if_VLambda_in_VsetI:
  assumes "Limit \<alpha>" and "VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Coprod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
interpret vsv \<open>VLambda I A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (VLambda I A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<D>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
VLambda I A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (fastforce intro!: vdomain_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have I: "I \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. I \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<Coprod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<subseteq>\<^sub>\<circ> I \<times>\<^sub>\<circ> (\<Union>\<^sub>\<circ>(\<R>\<^sub>\<circ> (VLambda I A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VSigma I A \<subseteq>\<^sub>\<circ> I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
VSigma I A \<subseteq>\<^sub>\<circ> I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A))

goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
VSigma I A \<subseteq>\<^sub>\<circ> I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A))

goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "I \<times>\<^sub>\<circ> (\<Union>\<^sub>\<circ>(\<R>\<^sub>\<circ> (VLambda I A))) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro Limit_vtimes_in_VsetI assms I VUnion_in_VsetI vrange_in_VsetI)
[PROOF STATE]
proof (state)
this:
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
VSigma I A \<subseteq>\<^sub>\<circ> I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A))
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "(\<Coprod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
VSigma I A \<subseteq>\<^sub>\<circ> I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A))
I \<times>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I A)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VSigma I A \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vrange_vprojection_in_VsetI:
  assumes "Limit \<alpha>"
    and "A \<in>\<^sub>\<circ> Vset \<alpha>"
    and "\<And>f. f \<in>\<^sub>\<circ> A \<Longrightarrow> vsv f"
    and "\<And>f. f \<in>\<^sub>\<circ> A \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> f"
  shows "\<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
[PROOF STEP]
assume "y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>)"
[PROOF STATE]
proof (state)
this:
y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>)

goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>)
[PROOF STEP]
obtain f where f: "f \<in>\<^sub>\<circ> A" and y_def: "y = f\<lparr>x\<rparr>"
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> A; y = f\<lparr>x\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> A
y = f\<lparr>x\<rparr>

goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> A
[PROOF STEP]
have "vsv f" and "x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> f"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. vsv f &&& x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> f
[PROOF STEP]
by (auto intro: assms(3,4))+
[PROOF STATE]
proof (state)
this:
vsv f
x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> f

goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
[PROOF STEP]
with y_def
[PROOF STATE]
proof (chain)
picking this:
y = f\<lparr>x\<rparr>
vsv f
x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> f
[PROOF STEP]
have xy: "\<langle>x, y\<rangle> \<in>\<^sub>\<circ> f"
[PROOF STATE]
proof (prove)
using this:
y = f\<lparr>x\<rparr>
vsv f
x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> f

goal (1 subgoal):
 1. \<langle>x, y\<rangle> \<in>\<^sub>\<circ> f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>x, y\<rangle> \<in>\<^sub>\<circ> f

goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
[PROOF STEP]
show "y \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
[PROOF STEP]
proof(intro VUnionI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. ?x2 \<in>\<^sub>\<circ> A
 2. ?x1 \<in>\<^sub>\<circ> ?x2
 3. ?x \<in>\<^sub>\<circ> ?x1
 4. y \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "f \<in>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> A
[PROOF STEP]
by (rule f)
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> A

goal (3 subgoals):
 1. ?x1 \<in>\<^sub>\<circ> f
 2. ?x \<in>\<^sub>\<circ> ?x1
 3. y \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "\<langle>x, y\<rangle> \<in>\<^sub>\<circ> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x, y\<rangle> \<in>\<^sub>\<circ> f
[PROOF STEP]
by (rule xy)
[PROOF STATE]
proof (state)
this:
\<langle>x, y\<rangle> \<in>\<^sub>\<circ> f

goal (2 subgoals):
 1. ?x \<in>\<^sub>\<circ> \<langle>x, y\<rangle>
 2. y \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "set {x, y} \<in>\<^sub>\<circ> \<langle>x, y\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {x, y} \<in>\<^sub>\<circ> \<langle>x, y\<rangle>
[PROOF STEP]
unfolding vpair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {x, y} \<in>\<^sub>\<circ> set {set {x}, set {x, y}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set {x, y} \<in>\<^sub>\<circ> \<langle>x, y\<rangle>

goal (1 subgoal):
 1. y \<in>\<^sub>\<circ> set {x, y}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
y \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>A)) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro VUnion_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A))
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>A. f\<lparr>x\<rparr>) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vcpower_in_VsetI:
  assumes "Limit \<alpha>" and "n \<in>\<^sub>\<circ> Vset \<alpha>" and "A \<in>\<^sub>\<circ> Vset \<alpha>" and "vfinite n"
  shows "A ^\<^sub>\<times> n \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^\<^sub>\<times> n \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms Limit_vproduct_in_VsetI
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
n \<in>\<^sub>\<circ> Vset \<alpha>
A \<in>\<^sub>\<circ> Vset \<alpha>
vfinite n
\<lbrakk>Limit ?\<alpha>; ?I \<in>\<^sub>\<circ> Vset ?\<alpha>; \<And>i. i \<in>\<^sub>\<circ> ?I \<Longrightarrow> ?A i \<in>\<^sub>\<circ> Vset ?\<alpha>; vfinite ?I\<rbrakk> \<Longrightarrow> vproduct ?I ?A \<in>\<^sub>\<circ> Vset ?\<alpha>

goal (1 subgoal):
 1. A ^\<^sub>\<times> n \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding vcpower_def
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
n \<in>\<^sub>\<circ> Vset \<alpha>
A \<in>\<^sub>\<circ> Vset \<alpha>
vfinite n
\<lbrakk>Limit ?\<alpha>; ?I \<in>\<^sub>\<circ> Vset ?\<alpha>; \<And>i. i \<in>\<^sub>\<circ> ?I \<Longrightarrow> ?A i \<in>\<^sub>\<circ> Vset ?\<alpha>; vfinite ?I\<rbrakk> \<Longrightarrow> vproduct ?I ?A \<in>\<^sub>\<circ> Vset ?\<alpha>

goal (1 subgoal):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>n. A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma Limit_vfinite_in_VsetI:
  assumes "Limit \<alpha>" and "A \<subseteq>\<^sub>\<circ> Vset \<alpha>" and "vfinite A"
  shows "A \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
vfinite A
[PROOF STEP]
obtain n where n: "n \<in>\<^sub>\<circ> \<omega>" and "n \<approx>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
using this:
vfinite A

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; n \<approx>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
n \<in>\<^sub>\<circ> \<omega>
n \<approx>\<^sub>\<circ> A

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in>\<^sub>\<circ> \<omega>
n \<approx>\<^sub>\<circ> A
[PROOF STEP]
obtain f where f: "v11 f" and dr: "\<D>\<^sub>\<circ> f = n" "\<R>\<^sub>\<circ> f = A"
[PROOF STATE]
proof (prove)
using this:
n \<in>\<^sub>\<circ> \<omega>
n \<approx>\<^sub>\<circ> A

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>v11 f; \<D>\<^sub>\<circ> f = n; \<R>\<^sub>\<circ> f = A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v11 f
\<D>\<^sub>\<circ> f = n
\<R>\<^sub>\<circ> f = A

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
interpret f: v11 f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 f
[PROOF STEP]
by (rule f)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
n \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
have n: "vfinite n"
[PROOF STATE]
proof (prove)
using this:
n \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfinite n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfinite n

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule f.vsv_Limit_vrange_in_VsetI[simplified dr, OF assms(1,2) n])
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_omega_in_VsetI:
  assumes "Limit \<alpha>"
  shows "a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
[PROOF STEP]
have "\<alpha> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>

goal (1 subgoal):
 1. \<alpha> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<alpha> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<alpha> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<omega> \<subseteq>\<^sub>\<circ> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<subseteq>\<^sub>\<circ> \<alpha>
[PROOF STEP]
by (simp add: assms omega_le_Limit)
[PROOF STATE]
proof (state)
this:
\<omega> \<subseteq>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<omega> \<subseteq>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "a\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<subseteq>\<^sub>\<circ> Vset \<alpha>
\<omega> \<subseteq>\<^sub>\<circ> \<alpha>
a\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
show "a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<subseteq>\<^sub>\<circ> Vset \<alpha>
\<omega> \<subseteq>\<^sub>\<circ> \<alpha>
a\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_succ_in_VsetI:
  assumes "Limit \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "succ a \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: assms succ_def vinsert_in_VsetI)


[STATEMENT]
lemma (in vfsequence) vfsequence_Limit_vcons_in_VsetI:
  assumes "Limit \<alpha>" and "x \<in>\<^sub>\<circ> Vset \<alpha>" and "xs \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "vcons xs x \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert \<langle>vcard xs, x\<rangle> xs \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof(intro vinsert_in_VsetI Limit_vpair_in_VsetI assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard xs \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "vcard xs \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard xs \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (metis assms(3) vdomain_in_VsetI vfsequence_vdomain)
[PROOF STATE]
proof (state)
this:
vcard xs \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_ftimes_in_VsetI:
  assumes "Limit \<alpha>" and "A \<in>\<^sub>\<circ> Vset \<alpha>" and "B \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "A \<times>\<^sub>\<bullet> B \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<times>\<^sub>\<bullet> B \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding ftimes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof(rule Limit_vproduct_in_VsetI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. Limit \<alpha>
 2. 2\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
 3. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B) \<in>\<^sub>\<circ> Vset \<alpha>
 4. vfinite (2\<^sub>\<nat>)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
[PROOF STEP]
show "2\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>

goal (1 subgoal):
 1. 2\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (meson Limit_omega_in_VsetI)
[PROOF STATE]
proof (state)
this:
2\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>

goal (3 subgoals):
 1. Limit \<alpha>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B) \<in>\<^sub>\<circ> Vset \<alpha>
 3. vfinite (2\<^sub>\<nat>)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Limit \<alpha>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B) \<in>\<^sub>\<circ> Vset \<alpha>
 3. vfinite (2\<^sub>\<nat>)
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> 2\<^sub>\<nat>"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>

goal (3 subgoals):
 1. Limit \<alpha>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B) \<in>\<^sub>\<circ> Vset \<alpha>
 3. vfinite (2\<^sub>\<nat>)
[PROOF STEP]
with assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>
[PROOF STEP]
show "(i = 0 ? A : B) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>

goal (1 subgoal):
 1. (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B) \<in>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. Limit \<alpha>
 2. vfinite (2\<^sub>\<nat>)
[PROOF STEP]
qed (auto simp: assms(1))


[STATEMENT]
lemma vempty_in_Vset_succ[simp, intro]: "0 \<in>\<^sub>\<circ> Vfrom a (succ b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<in>\<^sub>\<circ> Vfrom a (ZFC_in_HOL.succ b)
[PROOF STEP]
unfolding Vfrom_succ
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<in>\<^sub>\<circ> a \<union>\<^sub>\<circ> VPow (Vfrom a b)
[PROOF STEP]
by force


[STATEMENT]
lemma Limit_vid_on_in_Vset:
  assumes "Limit \<alpha>" and "A \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "vid_on A \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vid_on A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by
    (
      rule vbrelation.vbrelation_Limit_in_VsetI
        [
          OF vbrelation_vid_on assms(1) ,
          unfolded vdomain_vid_on vrange_vid_on, OF assms(2,2)
        ]
    )


[STATEMENT]
lemma Ord_vpair_in_Vset_succI[intro]:
  assumes "Ord \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> Vset (succ (succ \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
unfolding vpair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {set {a}, set {a, b}} \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set {set {a}, set {a, b}} \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
have aab: "set {set {a}, set {a, b}} = vinsert (set {a}) (set {set {a, b}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {set {a}, set {a, b}} = vinsert (set {a}) (set {set {a, b}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set {set {a}, set {a, b}} = vinsert (set {a}) (set {set {a, b}})

goal (1 subgoal):
 1. set {set {a}, set {a, b}} \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
show "set {set {a}, set {a, b}} \<in>\<^sub>\<circ> Vset (succ (succ \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {set {a}, set {a, b}} \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
unfolding aab
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert (set {a}) (set {set {a, b}}) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
by
      (
        intro
          assms
          vinsert_in_Vset_succI'
          Ord_vsingleton_in_Vset_succI
          Ord_vdoubleton_in_Vset_succI
          Ord_succ
      )
[PROOF STATE]
proof (state)
this:
set {set {a}, set {a, b}} \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vifunion_vsubset_VsetI:
  assumes "Limit \<alpha>" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> A i \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
assume "x \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i)"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)
[PROOF STEP]
obtain i where i: "i \<in>\<^sub>\<circ> I" and "x \<in>\<^sub>\<circ> A i"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in>\<^sub>\<circ> I; x \<in>\<^sub>\<circ> A i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I
x \<in>\<^sub>\<circ> A i

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms(1) assms(2)[OF i]
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
A i \<in>\<^sub>\<circ> Vset \<alpha>
i \<in>\<^sub>\<circ> I
x \<in>\<^sub>\<circ> A i
[PROOF STEP]
show "x \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
A i \<in>\<^sub>\<circ> Vset \<alpha>
i \<in>\<^sub>\<circ> I
x \<in>\<^sub>\<circ> A i

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vproduct_vsubset_Vset_succI:
  assumes "Limit \<alpha>" and "I \<in>\<^sub>\<circ> Vset \<alpha>" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> A i \<subseteq>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<subseteq>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vproduct I A \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i)"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> vproduct I A

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
note a = vproductD[OF prems]
[PROOF STATE]
proof (state)
this:
vsv a
\<D>\<^sub>\<circ> a = I
\<forall>i\<in>elts I. a\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
interpret vsv a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv a
[PROOF STEP]
by (rule a(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> vproduct I A
[PROOF STEP]
have "\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> vproduct I A

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)
[PROOF STEP]
by (rule vproduct_vrange)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
have "(\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro vifunion_least assms(3))
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I)
\<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
from assms(2) prems
[PROOF STATE]
proof (chain)
picking this:
I \<in>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> vproduct I A
[PROOF STEP]
have "\<D>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
I \<in>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> vproduct I A

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding a(2)
[PROOF STATE]
proof (prove)
using this:
I \<in>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> vproduct I A

goal (1 subgoal):
 1. I \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>
\<D>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "a \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>
\<D>\<^sub>\<circ> a \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. a \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro assms(1) vbrelation_Limit_vsubset_VsetI)
[PROOF STATE]
proof (state)
this:
a \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> vproduct I A \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
a \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
a \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by (simp add: Limit_is_Ord Ord_vsubset_in_Vset_succI)
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vproduct_vsubset_Vset_succI':
  assumes "Limit \<alpha>" and "I \<in>\<^sub>\<circ> Vset \<alpha>" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> A i \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. A i) \<subseteq>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vproduct I A \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vproduct I A \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
have "A i \<subseteq>\<^sub>\<circ> Vset \<alpha>" if "i \<in>\<^sub>\<circ> I" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A i \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Vset_trans vsubsetI assms(3) that)
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> A ?i \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
from assms(1,2) this
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
I \<in>\<^sub>\<circ> Vset \<alpha>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> A ?i \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
I \<in>\<^sub>\<circ> Vset \<alpha>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> A ?i \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vproduct I A \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by (rule Limit_vproduct_vsubset_Vset_succI)
[PROOF STATE]
proof (state)
this:
vproduct I A \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_Ord_vcons_in_Vset_succI:
  assumes "Ord \<alpha>"
    and "\<omega> \<in>\<^sub>\<circ> \<alpha>"
    and "x \<in>\<^sub>\<circ> Vset \<alpha>"
    and "xs \<in>\<^sub>\<circ> Vset (succ (succ (succ \<alpha>)))"
  shows "vcons xs x \<in>\<^sub>\<circ> Vset (succ (succ (succ \<alpha>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>)))
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert \<langle>vcard xs, x\<rangle> xs \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>)))
[PROOF STEP]
proof(intro vinsert_in_Vset_succI' Ord_succ Ord_vpair_in_Vset_succI assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard xs \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "vcard xs = \<D>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard xs = \<D>\<^sub>\<circ> xs
[PROOF STEP]
by (simp add: vfsequence_vdomain)
[PROOF STATE]
proof (state)
this:
vcard xs = \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. vcard xs \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1,2) vfsequence_vdomain_in_omega
[PROOF STATE]
proof (chain)
picking this:
Ord \<alpha>
\<omega> \<in>\<^sub>\<circ> \<alpha>
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
show "vcard xs \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
\<omega> \<in>\<^sub>\<circ> \<alpha>
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vcard xs \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding vfsequence_vdomain[symmetric]
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
\<omega> \<in>\<^sub>\<circ> \<alpha>
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (meson Ord_in_in_VsetI Vset_trans)
[PROOF STATE]
proof (state)
this:
vcard xs \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_VUnion_vdomain_in_VsetI:
  assumes "Limit \<alpha>" and "Q \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Union>\<^sub>\<circ>r\<in>\<^sub>\<circ>Q. \<D>\<^sub>\<circ> r) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<Union>\<^sub>\<circ>r\<in>\<^sub>\<circ>Q. \<D>\<^sub>\<circ> r) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>r\<in>\<^sub>\<circ>Q. \<D>\<^sub>\<circ> r)"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q)
[PROOF STEP]
obtain r where r: "r \<in>\<^sub>\<circ> Q" and "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in>\<^sub>\<circ> Q; a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in>\<^sub>\<circ> Q
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
Q \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Q
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
[PROOF STEP]
obtain b where ab: "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
Q \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Q
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<And>b. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
proof(intro VUnionI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. ?x2 \<in>\<^sub>\<circ> Q
 2. ?x1 \<in>\<^sub>\<circ> ?x2
 3. ?x \<in>\<^sub>\<circ> ?x1
 4. a \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "r \<in>\<^sub>\<circ> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in>\<^sub>\<circ> Q
[PROOF STEP]
by (rule r)
[PROOF STATE]
proof (state)
this:
r \<in>\<^sub>\<circ> Q

goal (3 subgoals):
 1. ?x1 \<in>\<^sub>\<circ> r
 2. ?x \<in>\<^sub>\<circ> ?x1
 3. a \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> r
[PROOF STEP]
by (rule ab)
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> r

goal (2 subgoals):
 1. ?x \<in>\<^sub>\<circ> \<langle>a, b\<rangle>
 2. a \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "set {a, b} \<in>\<^sub>\<circ> \<langle>a, b\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> \<langle>a, b\<rangle>
[PROOF STEP]
unfolding vpair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> set {set {a}, set {a, b}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set {a, b} \<in>\<^sub>\<circ> \<langle>a, b\<rangle>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> set {a, b}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
Q \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>Q)) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Q \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (blast dest!: VUnion_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: vsubset_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda Q \<D>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_VUnion_vrange_in_VsetI:
  assumes "Limit \<alpha>" and "Q \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Union>\<^sub>\<circ>r\<in>\<^sub>\<circ>Q. \<R>\<^sub>\<circ> r) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
(*FIXME: duality*)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<Union>\<^sub>\<circ>r\<in>\<^sub>\<circ>Q. \<R>\<^sub>\<circ> r) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
assume "b \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>r\<in>\<^sub>\<circ>Q. \<R>\<^sub>\<circ> r)"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q)
[PROOF STEP]
obtain r where r: "r \<in>\<^sub>\<circ> Q" and "b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in>\<^sub>\<circ> Q; b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in>\<^sub>\<circ> Q
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
Q \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Q
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
obtain a where ab: "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
Q \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Q
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<And>a. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
show "b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
[PROOF STEP]
proof(intro VUnionI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. ?x2 \<in>\<^sub>\<circ> Q
 2. ?x1 \<in>\<^sub>\<circ> ?x2
 3. ?x \<in>\<^sub>\<circ> ?x1
 4. b \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "r \<in>\<^sub>\<circ> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in>\<^sub>\<circ> Q
[PROOF STEP]
by (rule r)
[PROOF STATE]
proof (state)
this:
r \<in>\<^sub>\<circ> Q

goal (3 subgoals):
 1. ?x1 \<in>\<^sub>\<circ> r
 2. ?x \<in>\<^sub>\<circ> ?x1
 3. b \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> r
[PROOF STEP]
by (rule ab)
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> r

goal (2 subgoals):
 1. ?x \<in>\<^sub>\<circ> \<langle>a, b\<rangle>
 2. b \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show "set {a, b} \<in>\<^sub>\<circ> \<langle>a, b\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> \<langle>a, b\<rangle>
[PROOF STEP]
unfolding vpair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> set {set {a}, set {a, b}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set {a, b} \<in>\<^sub>\<circ> \<langle>a, b\<rangle>

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> set {a, b}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
Q \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>Q)) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Q \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (blast dest!: VUnion_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q))
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> Q)) \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: vsubset_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (VLambda Q \<R>\<^sub>\<circ> `\<^sub>\<circ> Q) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vempty_Z_def: "0 = set {x. x \<noteq> x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> = set {x. x \<noteq> x}
[PROOF STEP]
by auto


[STATEMENT]
lemma vempty_is_zet[intro, simp]: "0 \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using Vset_in_mono omega_in_\<alpha>
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> ?j \<Longrightarrow> Vset ?i \<in>\<^sub>\<circ> Vset ?j
\<omega> \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. []\<^sub>\<circ> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma Axiom_of_Extensionality:
  assumes "a \<in>\<^sub>\<circ> Vset \<alpha>" and "x = y" and "x \<in>\<^sub>\<circ> a"
  shows "y \<in>\<^sub>\<circ> a" and "x \<in>\<^sub>\<circ> Vset \<alpha>" and "y \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in>\<^sub>\<circ> a &&& x \<in>\<^sub>\<circ> Vset \<alpha> &&& y \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>
x = y
x \<in>\<^sub>\<circ> a

goal (1 subgoal):
 1. y \<in>\<^sub>\<circ> a &&& x \<in>\<^sub>\<circ> Vset \<alpha> &&& y \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp_all add: Vset_trans)


[STATEMENT]
lemma Axiom_of_Pairing:
  assumes "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Limit_vdoubleton_in_VsetI)


[STATEMENT]
lemma Axiom_of_Unions:
  assumes "a \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "\<Union>\<^sub>\<circ>a \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: VUnion_in_VsetI)


[STATEMENT]
lemma Axiom_of_Powers:
  assumes "a \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "VPow a \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VPow a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VPow a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Limit_VPow_in_VsetI)


[STATEMENT]
lemma Axiom_of_Regularity:
  assumes "a \<noteq> 0" and "a \<in>\<^sub>\<circ> Vset \<alpha>"
  obtains x where "x \<in>\<^sub>\<circ> a" and "x \<inter>\<^sub>\<circ> a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>\<^sub>\<circ> a; x \<inter>\<^sub>\<circ> a = []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> []\<^sub>\<circ>
a \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>\<^sub>\<circ> a; x \<inter>\<^sub>\<circ> a = []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: trad_foundation)


[STATEMENT]
lemma Axiom_of_Infinity: "\<omega> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using Limit_is_Ord
[PROOF STATE]
proof (prove)
using this:
Limit ?\<xi> \<Longrightarrow> Ord ?\<xi>

goal (1 subgoal):
 1. \<omega> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: Ord_iff_rank Ord_VsetI OrdmemD)


[STATEMENT]
lemma Axiom_of_Choice:
  assumes "A \<in>\<^sub>\<circ> Vset \<alpha>"
  obtains f where "f \<in>\<^sub>\<circ> Vset \<alpha>" and "\<And>x. x \<in>\<^sub>\<circ> A \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define f where "f = (\<lambda>x\<in>\<^sub>\<circ>A. (SOME a. a \<in>\<^sub>\<circ> x \<or> (x = 0 \<and> a = 0)))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>x\<in>\<^sub>\<circ>A. SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret vsv f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv f
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>x\<in>\<^sub>\<circ>A. SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have A_def: "A = \<D>\<^sub>\<circ> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = \<D>\<^sub>\<circ> f
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = \<D>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A = \<D>\<^sub>\<circ> f

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have Rf: "\<R>\<^sub>\<circ> f \<subseteq>\<^sub>\<circ> vinsert 0 (\<Union>\<^sub>\<circ>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> f \<subseteq>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
proof(rule vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f \<Longrightarrow> x \<in>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f \<Longrightarrow> x \<in>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
assume "y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f"
[PROOF STATE]
proof (state)
this:
y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f \<Longrightarrow> x \<in>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f
[PROOF STEP]
obtain x where "x \<in>\<^sub>\<circ> A" and "y = f\<lparr>x\<rparr>"
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; y = f\<lparr>x\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> f; y = f\<lparr>x\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: vrange_atD)
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> A
y = f\<lparr>x\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f \<Longrightarrow> x \<in>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> A
y = f\<lparr>x\<rparr>
[PROOF STEP]
have y_def: "y = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = 0 \<and> a = 0)"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A
y = f\<lparr>x\<rparr>

goal (1 subgoal):
 1. y = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A
y = (\<lambda>x\<in>\<^sub>\<circ>A. SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)\<lparr>x\<rparr>

goal (1 subgoal):
 1. y = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> f
y = (\<lambda>x\<in>\<^sub>\<circ>\<D>\<^sub>\<circ> f. SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)\<lparr>x\<rparr>

goal (1 subgoal):
 1. y = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f \<Longrightarrow> x \<in>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
have "y = 0 \<or> y \<in>\<^sub>\<circ> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x
[PROOF STEP]
proof(cases \<open>x = 0\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = []\<^sub>\<circ> \<Longrightarrow> y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x
 2. x \<noteq> []\<^sub>\<circ> \<Longrightarrow> y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> []\<^sub>\<circ>

goal (2 subgoals):
 1. x = []\<^sub>\<circ> \<Longrightarrow> y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x
 2. x \<noteq> []\<^sub>\<circ> \<Longrightarrow> y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> []\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> []\<^sub>\<circ>

goal (1 subgoal):
 1. y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> []\<^sub>\<circ>

goal (1 subgoal):
 1. (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>) = []\<^sub>\<circ> \<or> (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>) \<in>\<^sub>\<circ> x
[PROOF STEP]
by (metis (mono_tags, lifting) verit_sko_ex' vemptyE)
[PROOF STATE]
proof (state)
this:
y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x

goal (1 subgoal):
 1. x = []\<^sub>\<circ> \<Longrightarrow> y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x
[PROOF STEP]
qed (simp add: y_def)
[PROOF STATE]
proof (state)
this:
y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> f \<Longrightarrow> x \<in>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
with \<open>x \<in>\<^sub>\<circ> A\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> A
y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x
[PROOF STEP]
show "y \<in>\<^sub>\<circ> vinsert 0 (\<Union>\<^sub>\<circ>A)"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A
y = []\<^sub>\<circ> \<or> y \<in>\<^sub>\<circ> x

goal (1 subgoal):
 1. y \<in>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
y \<in>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> f \<subseteq>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<Union>\<^sub>\<circ>A \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Axiom_of_Unions)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with vempty_is_zet Limit_\<alpha>
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
\<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "vinsert 0 (\<Union>\<^sub>\<circ>A) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
\<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with Rf
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> f \<subseteq>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<R>\<^sub>\<circ> f \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> f \<subseteq>\<^sub>\<circ> vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A)
vinsert []\<^sub>\<circ> (\<Union>\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> f \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> f \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with Limit_\<alpha> assms[unfolded A_def]
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
\<D>\<^sub>\<circ> f \<in>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> f \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "f \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
\<D>\<^sub>\<circ> f \<in>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> f \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x \<in>\<^sub>\<circ> A \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x
[PROOF STEP]
assume prems: "x \<in>\<^sub>\<circ> A" "x \<noteq> 0"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> A
x \<noteq> []\<^sub>\<circ>

goal (1 subgoal):
 1. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> A
x \<noteq> []\<^sub>\<circ>
[PROOF STEP]
have "f\<lparr>x\<rparr> = (SOME a. a \<in>\<^sub>\<circ> x \<or> (x = 0 \<and> a = 0))"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A
x \<noteq> []\<^sub>\<circ>

goal (1 subgoal):
 1. f\<lparr>x\<rparr> = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A
x \<noteq> []\<^sub>\<circ>

goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)\<lparr>x\<rparr> = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f\<lparr>x\<rparr> = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)

goal (1 subgoal):
 1. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x
[PROOF STEP]
with prems(2)
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> []\<^sub>\<circ>
f\<lparr>x\<rparr> = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)
[PROOF STEP]
show "f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> []\<^sub>\<circ>
f\<lparr>x\<rparr> = (SOME a. a \<in>\<^sub>\<circ> x \<or> x = []\<^sub>\<circ> \<and> a = []\<^sub>\<circ>)

goal (1 subgoal):
 1. f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x
[PROOF STEP]
by (metis (mono_tags, lifting) someI_ex vemptyE)
[PROOF STATE]
proof (state)
this:
f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in>\<^sub>\<circ> A; ?x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>?x\<rparr> \<in>\<^sub>\<circ> ?x

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Vset \<alpha>; \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> A; x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>x\<rparr> \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>?x \<in>\<^sub>\<circ> A; ?x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>?x\<rparr> \<in>\<^sub>\<circ> ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>?x \<in>\<^sub>\<circ> A; ?x \<noteq> []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> f\<lparr>?x\<rparr> \<in>\<^sub>\<circ> ?x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (simp add: that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in \<Z>) Ord_\<alpha>: "Ord \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord \<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma (in \<Z>) \<Z>_Vset_\<omega>2_vsubset_Vset: "Vset (\<omega> + \<omega>) \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vset (\<omega> + \<omega>) \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Vset_vsubset_mono omega2_vsubset_Limit)


[STATEMENT]
lemma (in \<Z>) \<Z>_Limit_\<alpha>\<omega>: "Limit (\<alpha> + \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Limit (\<alpha> + \<omega>)
[PROOF STEP]
by (simp add: Limit_is_Ord)


[STATEMENT]
lemma (in \<Z>) \<Z>_\<alpha>_\<alpha>\<omega>: "\<alpha> \<in>\<^sub>\<circ> \<alpha> + \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<in>\<^sub>\<circ> \<alpha> + \<omega>
[PROOF STEP]
by (simp add: Limit_is_Ord Ord_mem_iff_lt)


[STATEMENT]
lemma (in \<Z>) \<Z>_\<omega>_\<alpha>\<omega>: "\<omega> \<in>\<^sub>\<circ> \<alpha> + \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<in>\<^sub>\<circ> \<alpha> + \<omega>
[PROOF STEP]
using add_le_cancel_left0
[PROOF STATE]
proof (prove)
using this:
?x \<subseteq>\<^sub>\<circ> ?x + ?z

goal (1 subgoal):
 1. \<omega> \<in>\<^sub>\<circ> \<alpha> + \<omega>
[PROOF STEP]
by blast


[STATEMENT]
lemma \<Z>_\<omega>\<omega>: "\<Z> (\<omega> + \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> (\<omega> + \<omega>)
[PROOF STEP]
using \<omega>_gt0
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<subset>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. \<Z> (\<omega> + \<omega>)
[PROOF STEP]
by (auto intro: \<Z>.intro simp: Ord_mem_iff_lt)


[STATEMENT]
lemma (in \<Z>) in_omega_in_omega_plus[intro]:
  assumes "a \<in>\<^sub>\<circ> \<omega>"
  shows "a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
have "a \<in>\<^sub>\<circ> Vset \<omega>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<omega>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> Vset \<omega>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> Vset \<omega>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)
[PROOF STEP]
have "Vset \<omega> \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vset \<omega> \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)
[PROOF STEP]
by (simp add: Vset_in_mono \<Z>_\<omega>_\<alpha>\<omega>)
[PROOF STATE]
proof (state)
this:
Vset \<omega> \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> Vset \<omega>
Vset \<omega> \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)
[PROOF STEP]
show "a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<omega>
Vset \<omega> \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> Vset (\<alpha> + \<omega>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in \<Z>) ord_of_nat_in_Vset[simp]: "a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by force


[STATEMENT]
lemma (in \<Z>) vfsequences_on_in_VsetI:
  assumes "X \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "vfsequences_on X \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequences_on X \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vfsequences_on X \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from vfsequences_on_subset_\<omega>_set
[PROOF STATE]
proof (chain)
picking this:
{x. vfsequence x \<and> (\<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> ?X)} \<subseteq> elts (VPow (\<omega> \<times>\<^sub>\<circ> ?X))
[PROOF STEP]
have "vfsequences_on X \<subseteq>\<^sub>\<circ> VPow (\<omega> \<times>\<^sub>\<circ> X)"
[PROOF STATE]
proof (prove)
using this:
{x. vfsequence x \<and> (\<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> ?X)} \<subseteq> elts (VPow (\<omega> \<times>\<^sub>\<circ> ?X))

goal (1 subgoal):
 1. vfsequences_on X \<subseteq>\<^sub>\<circ> VPow (\<omega> \<times>\<^sub>\<circ> X)
[PROOF STEP]
by (auto simp: less_eq_V_def)
[PROOF STATE]
proof (state)
this:
vfsequences_on X \<subseteq>\<^sub>\<circ> VPow (\<omega> \<times>\<^sub>\<circ> X)

goal (1 subgoal):
 1. vfsequences_on X \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vfsequences_on X \<subseteq>\<^sub>\<circ> VPow (\<omega> \<times>\<^sub>\<circ> X)

goal (1 subgoal):
 1. vfsequences_on X \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "VPow (\<omega> \<times>\<^sub>\<circ> X) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VPow (\<omega> \<times>\<^sub>\<circ> X) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro Limit_VPow_in_VsetI Limit_vtimes_in_VsetI assms Axiom_of_Infinity)
      auto
[PROOF STATE]
proof (state)
this:
VPow (\<omega> \<times>\<^sub>\<circ> X) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vfsequences_on X \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vfsequences_on X \<subseteq>\<^sub>\<circ> VPow (\<omega> \<times>\<^sub>\<circ> X)
VPow (\<omega> \<times>\<^sub>\<circ> X) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vfsequences_on X \<subseteq>\<^sub>\<circ> VPow (\<omega> \<times>\<^sub>\<circ> X)
VPow (\<omega> \<times>\<^sub>\<circ> X) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vfsequences_on X \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfsequences_on X \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_mk_doubleton: "inj_on (mk_doubleton X) (elts X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (mk_doubleton X) (elts X)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> X; y \<in>\<^sub>\<circ> X; mk_doubleton X x = mk_doubleton X y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> X; y \<in>\<^sub>\<circ> X; mk_doubleton X x = mk_doubleton X y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "mk_doubleton X a = mk_doubleton X b"
[PROOF STATE]
proof (state)
this:
mk_doubleton X a = mk_doubleton X b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> X; y \<in>\<^sub>\<circ> X; mk_doubleton X x = mk_doubleton X y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mk_doubleton X a = mk_doubleton X b
[PROOF STEP]
have "{a, X} = {b, X}"
[PROOF STATE]
proof (prove)
using this:
mk_doubleton X a = mk_doubleton X b

goal (1 subgoal):
 1. {a, X} = {b, X}
[PROOF STEP]
unfolding mk_doubleton_def
[PROOF STATE]
proof (prove)
using this:
set {a, X} = set {b, X}

goal (1 subgoal):
 1. {a, X} = {b, X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a, X} = {b, X}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> X; y \<in>\<^sub>\<circ> X; mk_doubleton X x = mk_doubleton X y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{a, X} = {b, X}
[PROOF STEP]
show "a = b"
[PROOF STATE]
proof (prove)
using this:
{a, X} = {b, X}

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (metis doubleton_eq_iff)
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed