[STATEMENT]
lemma VUnion_in_VsetI[intro]:
  assumes "A \<in>\<^sub>\<circ> Vset i"
  shows "\<Union>\<^sub>\<circ>A \<in>\<^sub>\<circ> Vset i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
define i' where "i' = rank i"
[PROOF STATE]
proof (state)
this:
i' = rank i

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
note rank_conv = Vfrom_Ord_bundle[OF refl[of 0] refl[of i], folded i'_def]
[PROOF STATE]
proof (state)
this:
Vset i = Vset i'
Ord i'

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
from rank_conv(2) assms
[PROOF STATE]
proof (chain)
picking this:
Ord i'
A \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Ord i'
A \<in>\<^sub>\<circ> Vset i

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
unfolding rank_conv
[PROOF STATE]
proof (prove)
using this:
Ord i'
A \<in>\<^sub>\<circ> Vset i'

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset i'
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. A \<in>\<^sub>\<circ> Vset []\<^sub>\<circ> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; A \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>; A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; A \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<xi>; A \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
case (succ \<alpha>)
[PROOF STATE]
proof (state)
this:
Ord \<alpha>
A \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>
A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)

goal (3 subgoals):
 1. A \<in>\<^sub>\<circ> Vset []\<^sub>\<circ> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; A \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>; A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; A \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<xi>; A \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
show "\<Union>\<^sub>\<circ>A \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by (metis succ(1,3) VPow_iff VUnion_least Vset_trans Vset_succ)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)

goal (2 subgoals):
 1. A \<in>\<^sub>\<circ> Vset []\<^sub>\<circ> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; A \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<xi>; A \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
qed (auto simp: vrange_VLambda vimage_VLambda_vrange_rep Limit_Vfrom_eq)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_VUnion_in_VsetD:
  assumes "Limit \<alpha>" and "\<Union>\<^sub>\<circ>A \<in>\<^sub>\<circ> Vset \<alpha>"
  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]
have "A \<subseteq>\<^sub>\<circ> VPow (\<Union>\<^sub>\<circ>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq>\<^sub>\<circ> VPow (\<Union>\<^sub>\<circ> A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<subseteq>\<^sub>\<circ> VPow (\<Union>\<^sub>\<circ> A)

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma VInter_in_VsetI[intro]:
  assumes "A \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "\<Inter>\<^sub>\<circ>A \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Inter>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have subset: "\<Inter>\<^sub>\<circ>A \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ>A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter>\<^sub>\<circ> A \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Inter>\<^sub>\<circ> A \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> A

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

goal (1 subgoal):
 1. \<Inter>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>
[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 (rule VUnion_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> A \<in>\<^sub>\<circ> Vset \<alpha>

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vsingleton_in_VsetI[intro]:
  assumes "Limit \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "set {a} \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set {a} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have aa: "set {a} \<subseteq>\<^sub>\<circ> VPow a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a} \<subseteq>\<^sub>\<circ> VPow a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set {a} \<subseteq>\<^sub>\<circ> VPow a

goal (1 subgoal):
 1. set {a} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
[PROOF STEP]
have "Ord \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>

goal (1 subgoal):
 1. Ord \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ord \<alpha>

goal (1 subgoal):
 1. set {a} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from vsubset_in_VsetI[OF aa Limit_VPow_in_VsetI[OF assms(1)]]
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> set {a} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> set {a} \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. set {a} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Limit_is_Ord assms(2))
[PROOF STATE]
proof (state)
this:
set {a} \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


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

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


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

goal (1 subgoal):
 1. set {a} \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by (simp add: Vset_succ vsubset_vsingleton_leftI)


[STATEMENT]
lemma Limit_vdoubleton_in_VsetI[intro]:
  assumes "Limit \<alpha>" and "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]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
[PROOF STEP]
have "Ord \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>

goal (1 subgoal):
 1. Ord \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ord \<alpha>

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "a \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>\<xi>\<in>\<^sub>\<circ>\<alpha>. Vset \<xi>)" and "b \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>\<xi>\<in>\<^sub>\<circ>\<alpha>. Vset \<xi>)"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>) &&& b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
[PROOF STEP]
by (simp_all add: SUP_vifunion[symmetric] Limit_Vfrom_eq)
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
[PROOF STEP]
obtain A B
    where a: "a \<in>\<^sub>\<circ> Vset A" and "A \<in>\<^sub>\<circ> \<alpha>" and b: "b \<in>\<^sub>\<circ> Vset B" and "B \<in>\<^sub>\<circ> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>a \<in>\<^sub>\<circ> Vset A; A \<in>\<^sub>\<circ> \<alpha>; b \<in>\<^sub>\<circ> Vset B; B \<in>\<^sub>\<circ> \<alpha>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> Vset A
A \<in>\<^sub>\<circ> \<alpha>
b \<in>\<^sub>\<circ> Vset B
B \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> Vset A
A \<in>\<^sub>\<circ> \<alpha>
b \<in>\<^sub>\<circ> Vset B
B \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> Vset A
A \<in>\<^sub>\<circ> \<alpha>
b \<in>\<^sub>\<circ> Vset B
B \<in>\<^sub>\<circ> \<alpha>
[PROOF STEP]
have "Ord A" and "Ord B"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> Vset A
A \<in>\<^sub>\<circ> \<alpha>
b \<in>\<^sub>\<circ> Vset B
B \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. Ord A &&& Ord B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ord A
Ord B

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> Vset A
A \<in>\<^sub>\<circ> \<alpha>
b \<in>\<^sub>\<circ> Vset B
B \<in>\<^sub>\<circ> \<alpha>
Ord A
Ord B
[PROOF STEP]
have "A \<union>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset A
A \<in>\<^sub>\<circ> \<alpha>
b \<in>\<^sub>\<circ> Vset B
B \<in>\<^sub>\<circ> \<alpha>
Ord A
Ord B

goal (1 subgoal):
 1. A \<union>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<alpha>
[PROOF STEP]
by (metis Ord_linear_le le_iff_sup sup.order_iff)
[PROOF STATE]
proof (state)
this:
A \<union>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<union>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<alpha>
[PROOF STEP]
have "Vset (A \<union>\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
A \<union>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<alpha>

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

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Vset (A \<union>\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> Vset A
b \<in>\<^sub>\<circ> Vset B
[PROOF STEP]
have "set {a, b} \<subseteq>\<^sub>\<circ> Vset (A \<union>\<^sub>\<circ> B)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset A
b \<in>\<^sub>\<circ> Vset B

goal (1 subgoal):
 1. set {a, b} \<subseteq>\<^sub>\<circ> Vset (A \<union>\<^sub>\<circ> B)
[PROOF STEP]
by (simp add: Vfrom_sup vsubset_vdoubleton_leftI)
[PROOF STATE]
proof (state)
this:
set {a, b} \<subseteq>\<^sub>\<circ> Vset (A \<union>\<^sub>\<circ> B)

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Vset (A \<union>\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>
set {a, b} \<subseteq>\<^sub>\<circ> Vset (A \<union>\<^sub>\<circ> B)
[PROOF STEP]
show "set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Vset (A \<union>\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>
set {a, b} \<subseteq>\<^sub>\<circ> Vset (A \<union>\<^sub>\<circ> B)

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule vsubset_in_VsetI[rotated 1])
[PROOF STATE]
proof (state)
this:
set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha> &&& b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto intro!: Vset_trans[of _ \<open>set {a, b}\<close>])


[STATEMENT]
lemma Ord_vdoubleton_in_Vset_succI:
  assumes "Ord \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "set {a, b} \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by
    (
      meson
        assms Ord_Vset_in_Vset_succI vsubset_in_VsetI vsubset_vdoubleton_leftI
    )


[STATEMENT]
lemma vunion_in_VsetI[intro]:
  assumes "a \<in>\<^sub>\<circ> Vset i" and "b \<in>\<^sub>\<circ> Vset i"
  shows "a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
define i' where "i' = rank i"
[PROOF STATE]
proof (state)
this:
i' = rank i

goal (1 subgoal):
 1. a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
note rank_conv = Vfrom_Ord_bundle[OF refl[of 0] refl[of i], folded i'_def]
[PROOF STATE]
proof (state)
this:
Vset i = Vset i'
Ord i'

goal (1 subgoal):
 1. a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
using rank_conv(2) assms
[PROOF STATE]
proof (prove)
using this:
Ord i'
a \<in>\<^sub>\<circ> Vset i
b \<in>\<^sub>\<circ> Vset i

goal (1 subgoal):
 1. a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
unfolding rank_conv
[PROOF STATE]
proof (prove)
using this:
Ord i'
a \<in>\<^sub>\<circ> Vset i'
b \<in>\<^sub>\<circ> Vset i'

goal (1 subgoal):
 1. a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i'
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>a \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>; b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; \<lbrakk>a \<in>\<^sub>\<circ> Vset \<alpha>; b \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>; a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>); b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; a \<in>\<^sub>\<circ> Vset \<xi>; b \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<xi>; a \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)); b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
case (Limit \<alpha>)
[PROOF STATE]
proof (state)
this:
Limit \<alpha>
\<lbrakk>?\<xi> \<in>\<^sub>\<circ> \<alpha>; a \<in>\<^sub>\<circ> Vset ?\<xi>; b \<in>\<^sub>\<circ> Vset ?\<xi>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset ?\<xi>
a \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))

goal (3 subgoals):
 1. \<lbrakk>a \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>; b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; \<lbrakk>a \<in>\<^sub>\<circ> Vset \<alpha>; b \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>; a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>); b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; a \<in>\<^sub>\<circ> Vset \<xi>; b \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<xi>; a \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)); b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
from Limit
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
\<lbrakk>?\<xi> \<in>\<^sub>\<circ> \<alpha>; a \<in>\<^sub>\<circ> Vset ?\<xi>; b \<in>\<^sub>\<circ> Vset ?\<xi>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset ?\<xi>
a \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
have "set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
\<lbrakk>?\<xi> \<in>\<^sub>\<circ> \<alpha>; a \<in>\<^sub>\<circ> Vset ?\<xi>; b \<in>\<^sub>\<circ> Vset ?\<xi>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset ?\<xi>
a \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))

goal (1 subgoal):
 1. set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro Limit_vdoubleton_in_VsetI; unfold SUP_vifunion[symmetric])
        simp_all
[PROOF STATE]
proof (state)
this:
set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>

goal (3 subgoals):
 1. \<lbrakk>a \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>; b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; \<lbrakk>a \<in>\<^sub>\<circ> Vset \<alpha>; b \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>; a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>); b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; a \<in>\<^sub>\<circ> Vset \<xi>; b \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<xi>; a \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)); b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<Union>\<^sub>\<circ>(set {a, b}) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
set {a, b} \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (set {a, b}) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (blast intro: Limit.hyps)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> (set {a, b}) \<in>\<^sub>\<circ> Vset \<alpha>

goal (3 subgoals):
 1. \<lbrakk>a \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>; b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; \<lbrakk>a \<in>\<^sub>\<circ> Vset \<alpha>; b \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>; a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>); b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; a \<in>\<^sub>\<circ> Vset \<xi>; b \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<xi>; a \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)); b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
with Limit.hyps VUnion_vdoubleton
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
\<Union>\<^sub>\<circ> (set {?a, ?b}) = ?a \<union>\<^sub>\<circ> ?b
\<Union>\<^sub>\<circ> (set {a, b}) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>\<xi>\<in>\<^sub>\<circ>\<alpha>. Vset \<xi>)"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
\<Union>\<^sub>\<circ> (set {?a, ?b}) = ?a \<union>\<^sub>\<circ> ?b
\<Union>\<^sub>\<circ> (set {a, b}) \<in>\<^sub>\<circ> Vset \<alpha>

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

goal (3 subgoals):
 1. \<lbrakk>a \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>; b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; \<lbrakk>a \<in>\<^sub>\<circ> Vset \<alpha>; b \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>; a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>); b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; a \<in>\<^sub>\<circ> Vset \<xi>; b \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<xi>; a \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)); b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
[PROOF STEP]
show "a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>)"
[PROOF STATE]
proof (prove)
using this:
a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)

goal (1 subgoal):
 1. a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<alpha>. a) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
by (simp add: \<open>Limit \<alpha>\<close> Limit_Vfrom_eq)
[PROOF STATE]
proof (state)
this:
a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<alpha>. a) `\<^sub>\<circ> \<alpha>))

goal (2 subgoals):
 1. \<lbrakk>a \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>; b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; \<lbrakk>a \<in>\<^sub>\<circ> Vset \<alpha>; b \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>; a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>); b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
qed (auto simp add: Vset_succ)
[PROOF STATE]
proof (state)
this:
a \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset i

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha> &&& b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (meson vsubset_in_VsetI inf_sup_ord(3,4))+


[STATEMENT]
lemma vintersection_in_VsetI[intro]:
  assumes "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "a \<inter>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<inter>\<^sub>\<circ> 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. a \<inter>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (meson vsubset_in_VsetI inf_sup_ord(2))


[STATEMENT]
lemma vdiff_in_VsetI[intro]:
  assumes "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "a -\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a -\<^sub>\<circ> 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. a -\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma vinsert_in_VsetI[intro]:
  assumes "Limit \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have ab: "vinsert a b = set {a} \<union>\<^sub>\<circ> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert a b = set {a} \<union>\<^sub>\<circ> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vinsert a b = set {a} \<union>\<^sub>\<circ> b

goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "set {a} \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. set {a} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Limit_vsingleton_in_VsetI assms(1))
[PROOF STATE]
proof (state)
this:
set {a} \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from this assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set {a} \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
set {a} \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding ab
[PROOF STATE]
proof (prove)
using this:
set {a} \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. set {a} \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vinsert_in_Vset_succI[intro]:
  assumes "Ord \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "vinsert a b \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by blast


[STATEMENT]
lemma vinsert_in_Vset_succI'[intro]:
  assumes "Ord \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
  shows "vinsert a b \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
have ab: "vinsert a b = set {a} \<union>\<^sub>\<circ> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert a b = set {a} \<union>\<^sub>\<circ> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vinsert a b = set {a} \<union>\<^sub>\<circ> b

goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert a b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
unfolding ab
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {a} \<union>\<^sub>\<circ> b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by (intro vunion_in_VsetI Ord_vsingleton_in_Vset_succI assms)
[PROOF STATE]
proof (state)
this:
vinsert a b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vinsert_in_VsetD:
  assumes "vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha> &&& b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms Vset_trans
[PROOF STATE]
proof (prove)
using this:
vinsert a b \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>?x \<in>\<^sub>\<circ> ?X; ?X \<in>\<^sub>\<circ> Vset ?i\<rbrakk> \<Longrightarrow> ?x \<in>\<^sub>\<circ> Vset ?i

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


[STATEMENT]
lemma Limit_insert_in_VsetI:
  assumes [intro]: "Limit \<alpha>"
    and [simp]: "small x"
    and "set x \<in>\<^sub>\<circ> Vset \<alpha>"
    and [intro]: "a \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "set (insert a x) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insert a x) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (insert a x) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have ax: "set (insert a x) = vinsert a (set x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insert a x) = vinsert a (set x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (insert a x) = vinsert a (set x)

goal (1 subgoal):
 1. set (insert a x) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
small x
set x \<in>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
small x
set x \<in>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. set (insert a x) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding ax
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
small x
set x \<in>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vpair_in_VsetI[intro]:
  assumes "Limit \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms Limit_vdoubleton_in_VsetI Limit_vsingleton_in_VsetI
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>Limit ?\<alpha>; ?a \<in>\<^sub>\<circ> Vset ?\<alpha>; ?b \<in>\<^sub>\<circ> Vset ?\<alpha>\<rbrakk> \<Longrightarrow> set {?a, ?b} \<in>\<^sub>\<circ> Vset ?\<alpha>
\<lbrakk>Limit ?\<alpha>; ?a \<in>\<^sub>\<circ> Vset ?\<alpha>\<rbrakk> \<Longrightarrow> set {?a} \<in>\<^sub>\<circ> Vset ?\<alpha>

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding vpair_def
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
a \<in>\<^sub>\<circ> Vset \<alpha>
b \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>Limit ?\<alpha>; ?a \<in>\<^sub>\<circ> Vset ?\<alpha>; ?b \<in>\<^sub>\<circ> Vset ?\<alpha>\<rbrakk> \<Longrightarrow> set {?a, ?b} \<in>\<^sub>\<circ> Vset ?\<alpha>
\<lbrakk>Limit ?\<alpha>; ?a \<in>\<^sub>\<circ> Vset ?\<alpha>\<rbrakk> \<Longrightarrow> set {?a} \<in>\<^sub>\<circ> Vset ?\<alpha>

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


[STATEMENT]
lemma vpair_in_VsetD[intro]:
  assumes "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "a \<in>\<^sub>\<circ> Vset \<alpha>" and "b \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha> &&& b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha> &&& b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding vpair_def
[PROOF STATE]
proof (prove)
using this:
set {set {a}, set {a, b}} \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha> &&& b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (meson vdoubleton_in_VsetD)+


[STATEMENT]
lemma Limit_vtimes_in_VsetI[intro]:
  assumes "Limit \<alpha>" and "A \<in>\<^sub>\<circ> Vset \<alpha>" and "B \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "A \<times>\<^sub>\<circ> B \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<times>\<^sub>\<circ> B \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<times>\<^sub>\<circ> B \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
[PROOF STEP]
have "Ord \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>

goal (1 subgoal):
 1. Ord \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ord \<alpha>

goal (1 subgoal):
 1. A \<times>\<^sub>\<circ> B \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "VPow (VPow (A \<union>\<^sub>\<circ> B)) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VPow (VPow (A \<union>\<^sub>\<circ> B)) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: assms Limit_VPow_in_VsetI Limit_is_Ord vunion_in_VsetI)
[PROOF STATE]
proof (state)
this:
VPow (VPow (A \<union>\<^sub>\<circ> B)) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. A \<times>\<^sub>\<circ> B \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1) vsubset_in_VsetI[OF vtimes_vsubset_VPowVPow this]
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
A \<times>\<^sub>\<circ> B \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
A \<times>\<^sub>\<circ> B \<in>\<^sub>\<circ> Vset \<alpha>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vbrelation) vbrelation_Limit_in_VsetI[intro]:
  assumes "Limit \<alpha>" and "\<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>" and "\<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms vdomain_vrange_vtimes
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
\<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
r \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> r \<times>\<^sub>\<circ> \<R>\<^sub>\<circ> r

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


[STATEMENT]
lemma
  assumes "r \<in>\<^sub>\<circ> Vset \<alpha>"
  shows vdomain_in_VsetI: "\<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
    and vrange_in_VsetI: "\<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
    and vfield_in_VsetI: "\<F>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha> &&& \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha> &&& \<F>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 3. \<F>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<Union>\<^sub>\<circ>r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
r \<in>\<^sub>\<circ> Vset \<alpha>

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

goal (3 subgoals):
 1. \<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 3. \<F>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
r \<in>\<^sub>\<circ> Vset \<alpha>
\<Union>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have r: "\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>r) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
r \<in>\<^sub>\<circ> Vset \<alpha>
\<Union>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>

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

goal (3 subgoals):
 1. \<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 3. \<F>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from r assms(1) vfield_vsubset_VUnion2
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r) \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Vset \<alpha>
\<F>\<^sub>\<circ> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r)
[PROOF STEP]
show "\<F>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r) \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Vset \<alpha>
\<F>\<^sub>\<circ> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r)

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

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from r assms(1) vdomain_vsubset_VUnion2 vrange_vsubset_VUnion2
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r) \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Vset \<alpha>
\<D>\<^sub>\<circ> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r)
\<R>\<^sub>\<circ> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r)
[PROOF STEP]
show
    "\<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>" "\<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r) \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Vset \<alpha>
\<D>\<^sub>\<circ> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r)
\<R>\<^sub>\<circ> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vbrelation) vbrelation_Limit_vsubset_VsetI:
  assumes "Limit \<alpha>" and "\<D>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>" and "\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>"
  shows "r \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> r \<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> r \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
assume "x \<in>\<^sub>\<circ> r"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> r

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

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> r \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> r
[PROOF STEP]
obtain a b where x_def: "x = \<langle>a, b\<rangle>"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<And>a b. x = \<langle>a, b\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim vbrelation_vinE)
[PROOF STATE]
proof (state)
this:
x = \<langle>a, b\<rangle>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> r \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> r
x = \<langle>a, b\<rangle>
[PROOF STEP]
have "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r" and "b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> r
x = \<langle>a, b\<rangle>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r &&& b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

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

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
\<D>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<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
  assumes "r \<in>\<^sub>\<circ> Vset \<alpha>"
  shows fdomain_in_VsetI: "\<D>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>"
    and frange_in_VsetI: "\<R>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>"
    and ffield_in_VsetI: "\<F>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha> &&& \<R>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha> &&& \<F>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<D>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
 3. \<F>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<Union>\<^sub>\<circ>r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
r \<in>\<^sub>\<circ> Vset \<alpha>

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

goal (3 subgoals):
 1. \<D>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
 3. \<F>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
r \<in>\<^sub>\<circ> Vset \<alpha>
\<Union>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have r: "\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>r)) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
r \<in>\<^sub>\<circ> Vset \<alpha>
\<Union>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>

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

goal (3 subgoals):
 1. \<D>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
 3. \<F>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from r assms(1) fdomain_vsubset_VUnion2 frange_vsubset_VUnion2
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r)) \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Vset \<alpha>
\<D>\<^sub>\<bullet> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r))
\<R>\<^sub>\<bullet> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r))
[PROOF STEP]
show
    "\<D>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>" "\<R>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r)) \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Vset \<alpha>
\<D>\<^sub>\<bullet> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r))
\<R>\<^sub>\<bullet> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r))

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

goal (1 subgoal):
 1. \<F>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from r assms(1) ffield_vsubset_VUnion2
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r)) \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Vset \<alpha>
\<F>\<^sub>\<bullet> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r))
[PROOF STEP]
show "\<F>\<^sub>\<bullet> r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r)) \<in>\<^sub>\<circ> Vset \<alpha>
r \<in>\<^sub>\<circ> Vset \<alpha>
\<F>\<^sub>\<bullet> ?r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> ?r))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vsv) vsv_Limit_vrange_in_VsetI[intro]:
  assumes "Limit \<alpha>" and "\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>" and "vfinite (\<D>\<^sub>\<circ> r)"
  shows "\<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms(3,1,2) vsv_axioms
[PROOF STATE]
proof (prove)
using this:
vfinite (\<D>\<^sub>\<circ> r)
Limit \<alpha>
\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>
vsv r

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof(induction \<open>\<D>\<^sub>\<circ> r\<close> arbitrary: r rule: vfinite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>[]\<^sub>\<circ> = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
case vempty
[PROOF STATE]
proof (state)
this:
[]\<^sub>\<circ> = \<D>\<^sub>\<circ> r
Limit \<alpha>
\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>
vsv r

goal (2 subgoals):
 1. \<And>r. \<lbrakk>[]\<^sub>\<circ> = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
interpret r': vsv r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv r
[PROOF STEP]
by (rule vempty(4))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>[]\<^sub>\<circ> = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from vempty(1) r'.vlrestriction_vdomain
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> = \<D>\<^sub>\<circ> r
r \<restriction>\<^sup>l\<^sub>\<circ> \<D>\<^sub>\<circ> r = r
[PROOF STEP]
have "r = 0"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> = \<D>\<^sub>\<circ> r
r \<restriction>\<^sup>l\<^sub>\<circ> \<D>\<^sub>\<circ> r = r

goal (1 subgoal):
 1. r = []\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = []\<^sub>\<circ>

goal (2 subgoals):
 1. \<And>r. \<lbrakk>[]\<^sub>\<circ> = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from Vset_in_mono vempty.prems(1)
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> ?j \<Longrightarrow> Vset ?i \<in>\<^sub>\<circ> Vset ?j
Limit \<alpha>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> ?j \<Longrightarrow> Vset ?i \<in>\<^sub>\<circ> Vset ?j
Limit \<alpha>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding \<open>r = 0\<close>
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> ?j \<Longrightarrow> Vset ?i \<in>\<^sub>\<circ> Vset ?j
Limit \<alpha>

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

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
case (vinsert x F)
[PROOF STATE]
proof (state)
this:
vfinite F
x \<notin>\<^sub>\<circ> F
\<lbrakk>F = \<D>\<^sub>\<circ> ?r; Limit \<alpha>; \<R>\<^sub>\<circ> ?r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv ?r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> ?r \<in>\<^sub>\<circ> Vset \<alpha>
vinsert x F = \<D>\<^sub>\<circ> r
Limit \<alpha>
\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>
vsv r

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
interpret r': vsv r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv r
[PROOF STEP]
by (rule vinsert(7))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have RrF_Rr: "\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have F_DrF: "F = \<D>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = \<D>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)
[PROOF STEP]
unfolding vdomain_vlrestriction vinsert(4)[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = vinsert x F \<inter>\<^sub>\<circ> F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F = \<D>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
F = \<D>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
note assms(1)
[PROOF STATE]
proof (state)
this:
Limit \<alpha>

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Limit \<alpha>

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from RrF_Rr vinsert(6)
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r
\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r
\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>

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

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "vsv (r \<restriction>\<^sup>l\<^sub>\<circ> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (r \<restriction>\<^sup>l\<^sub>\<circ> F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vsv (r \<restriction>\<^sup>l\<^sub>\<circ> F)

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
F = \<D>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)
Limit \<alpha>
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> Vset \<alpha>
vsv (r \<restriction>\<^sup>l\<^sub>\<circ> F)
[PROOF STEP]
have RrF_V\<alpha>: "\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
F = \<D>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)
Limit \<alpha>
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> Vset \<alpha>
vsv (r \<restriction>\<^sup>l\<^sub>\<circ> F)

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule vinsert(3))
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<R>\<^sub>\<circ> r = vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> r = vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r \<Longrightarrow> xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
 2. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r \<Longrightarrow> xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
 2. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
assume "b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (2 subgoals):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r \<Longrightarrow> xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
 2. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
obtain a where "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r" and b_def: "b = r\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

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

goal (2 subgoals):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r \<Longrightarrow> xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
 2. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
with vinsert.hyps(4)
[PROOF STATE]
proof (chain)
picking this:
vinsert x F = \<D>\<^sub>\<circ> r
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
b = r\<lparr>a\<rparr>
[PROOF STEP]
have "a = x \<or> a \<in>\<^sub>\<circ> F"
[PROOF STATE]
proof (prove)
using this:
vinsert x F = \<D>\<^sub>\<circ> r
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
b = r\<lparr>a\<rparr>

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

goal (2 subgoals):
 1. \<And>xa. xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r \<Longrightarrow> xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
 2. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
with \<open>a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
a = x \<or> a \<in>\<^sub>\<circ> F
[PROOF STEP]
show "b \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
a = x \<or> a \<in>\<^sub>\<circ> F

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
a = x \<or> a \<in>\<^sub>\<circ> F

goal (1 subgoal):
 1. r\<lparr>a\<rparr> \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
[PROOF STEP]
by (blast dest: r'.vsv_vimageI1)
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))

goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
assume "b \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))

goal (1 subgoal):
 1. \<And>xa. xa \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F)) \<Longrightarrow> xa \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
with RrF_Rr r'.vsv_axioms vinsert.hyps(4)
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r
vsv r
vinsert x F = \<D>\<^sub>\<circ> r
b \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
[PROOF STEP]
show "b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r
vsv r
vinsert x F = \<D>\<^sub>\<circ> r
b \<in>\<^sub>\<circ> vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> r = vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> r = vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with vinsert.prems(2)
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> r = vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
[PROOF STEP]
have "r\<lparr>x\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> r = vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))

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

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r\<lparr>x\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (blast intro: RrF_V\<alpha>)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x F r. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>r. \<lbrakk>F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>; vinsert x F = \<D>\<^sub>\<circ> r; Limit \<alpha>; \<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>; vsv r\<rbrakk> \<Longrightarrow> \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> r = vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
r\<lparr>x\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "\<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> r = vinsert (r\<lparr>x\<rparr>) (\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F))
r\<lparr>x\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> (r \<restriction>\<^sup>l\<^sub>\<circ> F) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: vinsert.prems(1) vinsert_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vsv) vsv_Limit_vsv_in_VsetI[intro]:
  assumes "Limit \<alpha>"
    and "\<D>\<^sub>\<circ> r \<in>\<^sub>\<circ> Vset \<alpha>"
    and "\<R>\<^sub>\<circ> r \<subseteq>\<^sub>\<circ> Vset \<alpha>"
    and "vfinite (\<D>\<^sub>\<circ> r)"
  shows "r \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: assms vsv_Limit_vrange_in_VsetI vbrelation_Limit_in_VsetI)


[STATEMENT]
lemma Limit_vcomp_in_VsetI:
  assumes "Limit \<alpha>" and "r \<in>\<^sub>\<circ> Vset \<alpha>" and "s \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "r \<circ>\<^sub>\<circ> s \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<circ>\<^sub>\<circ> s \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof(rule vbrelation.vbrelation_Limit_in_VsetI; (intro assms(1))?)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vbrelation (r \<circ>\<^sub>\<circ> s)
 2. \<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>
 3. \<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "vbrelation (r \<circ>\<^sub>\<circ> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vbrelation (r \<circ>\<^sub>\<circ> s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vbrelation (r \<circ>\<^sub>\<circ> s)

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> s

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>
 2. \<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
s \<in>\<^sub>\<circ> Vset \<alpha>
\<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> s
[PROOF STEP]
show "\<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
s \<in>\<^sub>\<circ> Vset \<alpha>
\<D>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> s

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

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "\<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
r \<in>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
show "\<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
r \<in>\<^sub>\<circ> Vset \<alpha>
\<R>\<^sub>\<circ> (r \<circ>\<^sub>\<circ> s) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> r

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. \<Inter>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1) range assms(3)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
\<R>\<^sub>\<circ> (VLambda I A) \<subseteq>\<^sub>\<circ> Vset \<alpha>
vfinite I
[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:
Limit \<alpha>
\<R>\<^sub>\<circ> (VLambda I A) \<subseteq>\<^sub>\<circ> Vset \<alpha>
vfinite I

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule rel_VLambda.vsv_Limit_vrange_in_VsetI[unfolded vdomain_VLambda])
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Inter>\<^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. \<Inter>\<^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 "(\<Inter>\<^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. \<Inter>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Inter>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_vifunion_in_VsetI:
  assumes "Limit \<alpha>" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> A i \<in>\<^sub>\<circ> Vset \<alpha>" and "vfinite I"
  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:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> A ?i \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have range: "\<R>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. A i) \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> A ?i \<in>\<^sub>\<circ> Vset \<alpha>

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

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> (VLambda I A `\<^sub>\<circ> I) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1) range assms(3)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
\<R>\<^sub>\<circ> (VLambda I A) \<subseteq>\<^sub>\<circ> Vset \<alpha>
vfinite I
[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:
Limit \<alpha>
\<R>\<^sub>\<circ> (VLambda I A) \<subseteq>\<^sub>\<circ> Vset \<alpha>
vfinite I

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (VLambda I A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule rel_VLambda.vsv_Limit_vrange_in_VsetI[unfolded vdomain_VLambda])
[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