[STATEMENT]
lemma sum_case_Inr [simp]: "sum_case f g (Inr y) = g y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_case f g (ZFC_Cardinals.Inr y) = g y
[PROOF STEP]
by (simp add: sum_case_def is_sum_def)


[STATEMENT]
lemma is_sum_cases: "(\<exists>x. z = Inl x \<or> z = Inr x) \<or> \<not> is_sum z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. z = ZFC_Cardinals.Inl x \<or> z = ZFC_Cardinals.Inr x) \<or> \<not> is_sum z
[PROOF STEP]
by (auto simp: is_sum_def)


[STATEMENT]
lemma sum_case_split:
  "P (sum_case f g a) \<longleftrightarrow> (\<forall>x. a = Inl x \<longrightarrow> P(f x)) \<and> (\<forall>y. a = Inr y \<longrightarrow> P(g y)) \<and> (\<not> is_sum a \<longrightarrow> P undefined)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (sum_case f g a) = ((\<forall>x. a = ZFC_Cardinals.Inl x \<longrightarrow> P (f x)) \<and> (\<forall>y. a = ZFC_Cardinals.Inr y \<longrightarrow> P (g y)) \<and> (\<not> is_sum a \<longrightarrow> P undefined))
[PROOF STEP]
by (cases "is_sum a") (auto simp: is_sum_def)


[STATEMENT]
lemma sum_case_split_asm:
  "P (sum_case f g a) \<longleftrightarrow> \<not> ((\<exists>x. a = Inl x \<and> \<not> P(f x)) \<or> (\<exists>y. a = Inr y \<and> \<not> P(g y)) \<or> (\<not> is_sum a \<and> \<not> P undefined))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (sum_case f g a) = (\<not> ((\<exists>x. a = ZFC_Cardinals.Inl x \<and> \<not> P (f x)) \<or> (\<exists>y. a = ZFC_Cardinals.Inr y \<and> \<not> P (g y)) \<or> \<not> is_sum a \<and> \<not> P undefined))
[PROOF STEP]
by (auto simp: sum_case_split)


[STATEMENT]
lemma small_UN [simp,intro]:
  assumes A: "small A" and B: "\<And>x. x \<in> A \<Longrightarrow> small (B x)"
  shows "small (\<Union>x\<in>A. B x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
obtain a where "elts a \<approx> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. elts a \<approx> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms small_eqpoll)
[PROOF STATE]
proof (state)
this:
elts a \<approx> A

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts a \<approx> A
[PROOF STEP]
obtain f where f: "bij_betw f (elts a) A"
[PROOF STATE]
proof (prove)
using this:
elts a \<approx> A

goal (1 subgoal):
 1. (\<And>f. bij_betw f (elts a) A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eqpoll_def
[PROOF STATE]
proof (prove)
using this:
elts a \<approx> A
?A \<approx> ?B \<equiv> \<exists>f. bij_betw f ?A ?B

goal (1 subgoal):
 1. (\<And>f. bij_betw f (elts a) A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bij_betw f (elts a) A

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
have "\<exists>y. elts y \<approx> B x" if "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. elts y \<approx> B x
[PROOF STEP]
using B small_eqpoll that
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> small (B ?x)
small ?A = (\<exists>x. elts x \<approx> ?A)
x \<in> A

goal (1 subgoal):
 1. \<exists>y. elts y \<approx> B x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> \<exists>y. elts y \<approx> B ?x

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> A \<Longrightarrow> \<exists>y. elts y \<approx> B ?x
[PROOF STEP]
obtain g where g: "\<And>x. x \<in> A \<Longrightarrow> elts (g x) \<approx> B x"
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> \<exists>y. elts y \<approx> B ?x

goal (1 subgoal):
 1. (\<And>g. (\<And>x. x \<in> A \<Longrightarrow> elts (g x) \<approx> B x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> elts (g ?x) \<approx> B ?x

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
have sm: "small (Sigma (elts a) (elts \<circ> g \<circ> f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (Sigma (elts a) (elts \<circ> g \<circ> f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
small (Sigma (elts a) (elts \<circ> g \<circ> f))

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
have "(\<Union>x\<in>A. B x) \<lesssim> Sigma A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (B ` A) \<lesssim> Sigma A B
[PROOF STEP]
by (metis image_lepoll snd_image_Sigma)
[PROOF STATE]
proof (state)
this:
\<Union> (B ` A) \<lesssim> Sigma A B

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> (B ` A) \<lesssim> Sigma A B

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
have "...  \<lesssim> Sigma (elts a) (elts \<circ> g \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma (elts a) (elts \<circ> g \<circ> f)
[PROOF STEP]
by (smt (verit) Sigma_eqpoll_cong bij_betw_iff_bijections comp_apply eqpoll_imp_lepoll eqpoll_sym f g)
[PROOF STATE]
proof (state)
this:
Sigma A B \<lesssim> Sigma (elts a) (elts \<circ> g \<circ> f)

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Union> (B ` A) \<lesssim> Sigma (elts a) (elts \<circ> g \<circ> f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union> (B ` A) \<lesssim> Sigma (elts a) (elts \<circ> g \<circ> f)

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
using lepoll_small sm
[PROOF STATE]
proof (prove)
using this:
\<Union> (B ` A) \<lesssim> Sigma (elts a) (elts \<circ> g \<circ> f)
\<lbrakk>small ?Y; ?X \<lesssim> ?Y\<rbrakk> \<Longrightarrow> small ?X
small (Sigma (elts a) (elts \<circ> g \<circ> f))

goal (1 subgoal):
 1. small (\<Union> (B ` A))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
small (\<Union> (B ` A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_Union [simp,intro]:
  assumes "\<A> \<subseteq> Collect small" "small \<A>"
  shows "small (\<Union> \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (\<Union> \<A>)
[PROOF STEP]
using small_UN [of \<A> "\<lambda>x. x"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>small \<A>; \<And>x. x \<in> \<A> \<Longrightarrow> small x\<rbrakk> \<Longrightarrow> small (\<Union>x\<in>\<A>. x)
\<A> \<subseteq> Collect small
small \<A>

goal (1 subgoal):
 1. small (\<Union> \<A>)
[PROOF STEP]
by (simp add: subset_iff)


[STATEMENT]
lemma beta [simp]:
  assumes "x \<in> elts A"
  shows "app (VLambda A b) x = b x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app (VLambda A b) x = b x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> elts A

goal (1 subgoal):
 1. app (VLambda A b) x = b x
[PROOF STEP]
by (auto simp: VLambda_def app_def)


[STATEMENT]
lemma VPi_I:
  assumes "\<And>x. x \<in> elts A \<Longrightarrow> b x \<in> elts (B x)"
  shows "VLambda A b \<in> elts (VPi A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda A b \<in> elts (VPi A B)
[PROOF STEP]
proof (clarsimp simp: VPi_def, intro conjI impI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)} \<Longrightarrow> VLambda A b \<le> VSigma A B
 2. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)} \<Longrightarrow> elts A \<subseteq> Domain (pairs (VLambda A b))
 3. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)} \<Longrightarrow> single_valued (pairs (VLambda A b))
 4. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}
[PROOF STEP]
show "VLambda A b \<le> VSigma A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda A b \<le> VSigma A B
[PROOF STEP]
by (auto simp: assms VLambda_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
VLambda A b \<le> VSigma A B

goal (3 subgoals):
 1. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)} \<Longrightarrow> elts A \<subseteq> Domain (pairs (VLambda A b))
 2. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)} \<Longrightarrow> single_valued (pairs (VLambda A b))
 3. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}
[PROOF STEP]
show "elts A \<subseteq> Domain (pairs (VLambda A b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts A \<subseteq> Domain (pairs (VLambda A b))
[PROOF STEP]
by (force simp: VLambda_def pairs_iff_elts)
[PROOF STATE]
proof (state)
this:
elts A \<subseteq> Domain (pairs (VLambda A b))

goal (2 subgoals):
 1. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)} \<Longrightarrow> single_valued (pairs (VLambda A b))
 2. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}
[PROOF STEP]
show "single_valued (pairs (VLambda A b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued (pairs (VLambda A b))
[PROOF STEP]
by (auto simp: VLambda_def single_valued_def pairs_iff_elts)
[PROOF STATE]
proof (state)
this:
single_valued (pairs (VLambda A b))

goal (1 subgoal):
 1. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}
[PROOF STEP]
show "small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}
[PROOF STEP]
by (metis (mono_tags, lifting) down VPow_iff mem_Collect_eq subsetI)
[PROOF STATE]
proof (state)
this:
small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_pair:
  assumes f: "f \<in> elts (VPi A B)" and x: "x \<in> elts A"
  shows "\<langle>x, app f x\<rangle> \<in> elts f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x, app f x\<rangle> \<in> elts f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>x, app f x\<rangle> \<in> elts f
[PROOF STEP]
have "x \<in> Domain (pairs f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Domain (pairs f)
[PROOF STEP]
by (metis (no_types, lifting) VPi_def assms elts_of_set empty_iff mem_Collect_eq subsetD)
[PROOF STATE]
proof (state)
this:
x \<in> Domain (pairs f)

goal (1 subgoal):
 1. \<langle>x, app f x\<rangle> \<in> elts f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Domain (pairs f)
[PROOF STEP]
obtain y where y: "\<langle>x,y\<rangle> \<in> elts f"
[PROOF STATE]
proof (prove)
using this:
x \<in> Domain (pairs f)

goal (1 subgoal):
 1. (\<And>y. \<langle>x, y\<rangle> \<in> elts f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pairs_iff_elts
[PROOF STATE]
proof (prove)
using this:
x \<in> Domain (pairs f)
((?x, ?y) \<in> pairs ?z) = (\<langle>?x, ?y\<rangle> \<in> elts ?z)

goal (1 subgoal):
 1. (\<And>y. \<langle>x, y\<rangle> \<in> elts f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>x, y\<rangle> \<in> elts f

goal (1 subgoal):
 1. \<langle>x, app f x\<rangle> \<in> elts f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x, app f x\<rangle> \<in> elts f
[PROOF STEP]
unfolding app_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x, THE y. \<langle>x, y\<rangle> \<in> elts f\<rangle> \<in> elts f
[PROOF STEP]
proof (rule theI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<langle>x, ?a\<rangle> \<in> elts f
 2. \<And>xa. \<langle>x, xa\<rangle> \<in> elts f \<Longrightarrow> xa = ?a
[PROOF STEP]
show "\<langle>x, y\<rangle> \<in> elts f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x, y\<rangle> \<in> elts f
[PROOF STEP]
by (rule y)
[PROOF STATE]
proof (state)
this:
\<langle>x, y\<rangle> \<in> elts f

goal (1 subgoal):
 1. \<And>xa. \<langle>x, xa\<rangle> \<in> elts f \<Longrightarrow> xa = y
[PROOF STEP]
show "z = y" if "\<langle>x, z\<rangle> \<in> elts f" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = y
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f \<in> elts (VPi A B)

goal (1 subgoal):
 1. z = y
[PROOF STEP]
unfolding VPi_def
[PROOF STATE]
proof (prove)
using this:
f \<in> elts (set {f \<in> elts (VPow (VSigma A B)). elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)})

goal (1 subgoal):
 1. z = y
[PROOF STEP]
by (metis (mono_tags, lifting) that elts_of_set empty_iff mem_Collect_eq pairs_iff_elts single_valued_def y)
[PROOF STATE]
proof (state)
this:
\<langle>x, ?z\<rangle> \<in> elts f \<Longrightarrow> ?z = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>x, app f x\<rangle> \<in> elts f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma VPi_D:
  assumes f: "f \<in> elts (VPi A B)" and x: "x \<in> elts A"
  shows "app f x \<in> elts (B x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app f x \<in> elts (B x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. app f x \<in> elts (B x)
[PROOF STEP]
have "f \<le> VSigma A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<le> VSigma A B
[PROOF STEP]
by (metis (no_types, lifting) VPi_def elts_of_set empty_iff f VPow_iff mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
f \<le> VSigma A B

goal (1 subgoal):
 1. app f x \<in> elts (B x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<le> VSigma A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<le> VSigma A B

goal (1 subgoal):
 1. app f x \<in> elts (B x)
[PROOF STEP]
using apply_pair [OF assms]
[PROOF STATE]
proof (prove)
using this:
f \<le> VSigma A B
\<langle>x, app f x\<rangle> \<in> elts f

goal (1 subgoal):
 1. app f x \<in> elts (B x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
app f x \<in> elts (B x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma VPi_memberD:
  assumes f: "f \<in> elts (VPi A B)" and p: "p \<in> elts f"
  obtains x where "x \<in> elts A" "p = \<langle>x, app f x\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> elts A; p = \<langle>x, app f x\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> elts A; p = \<langle>x, app f x\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "f \<le> VSigma A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<le> VSigma A B
[PROOF STEP]
by (metis (no_types, lifting) VPi_def elts_of_set empty_iff f VPow_iff mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
f \<le> VSigma A B

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> elts A; p = \<langle>x, app f x\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<le> VSigma A B
[PROOF STEP]
obtain x y where "p = \<langle>x,y\<rangle>" "x \<in> elts A"
[PROOF STATE]
proof (prove)
using this:
f \<le> VSigma A B

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>p = \<langle>x, y\<rangle>; x \<in> elts A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
f \<le> VSigma A B
p \<in> elts f

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>p = \<langle>x, y\<rangle>; x \<in> elts A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = \<langle>x, y\<rangle>
x \<in> elts A

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> elts A; p = \<langle>x, app f x\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = \<langle>x, y\<rangle>
x \<in> elts A
[PROOF STEP]
have "y = app f x"
[PROOF STATE]
proof (prove)
using this:
p = \<langle>x, y\<rangle>
x \<in> elts A

goal (1 subgoal):
 1. y = app f x
[PROOF STEP]
by (metis (no_types, lifting) VPi_def apply_pair elts_of_set equals0D f mem_Collect_eq p pairs_iff_elts single_valuedD)
[PROOF STATE]
proof (state)
this:
y = app f x

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> elts A; p = \<langle>x, app f x\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = app f x
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
y = app f x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using \<open>p = \<langle>x, y\<rangle>\<close> \<open>x \<in> elts A\<close> that
[PROOF STATE]
proof (prove)
using this:
y = app f x
p = \<langle>x, y\<rangle>
x \<in> elts A
\<lbrakk>?x \<in> elts A; p = \<langle>?x, app f ?x\<rangle>\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fun_ext:
  assumes "f \<in> elts (VPi A B)" "g \<in> elts (VPi A B)" "\<And>x. x \<in> elts A \<Longrightarrow> app f x = app g x"
  shows "f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g
[PROOF STEP]
by (metis VPi_memberD V_equalityI apply_pair assms)


[STATEMENT]
lemma eta[simp]:
  assumes "f \<in> elts (VPi A B)"
  shows "VLambda A ((app)f) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda A (app f) = f
[PROOF STEP]
proof (rule fun_ext [OF _ assms])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. VLambda A (app f) \<in> elts (VPi A B)
 2. \<And>x. x \<in> elts A \<Longrightarrow> app (VLambda A (app f)) x = app f x
[PROOF STEP]
show "VLambda A (app f) \<in> elts (VPi A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda A (app f) \<in> elts (VPi A B)
[PROOF STEP]
using VPi_D VPi_I assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f \<in> elts (VPi ?A ?B); ?x \<in> elts ?A\<rbrakk> \<Longrightarrow> app ?f ?x \<in> elts (?B ?x)
(\<And>x. x \<in> elts ?A \<Longrightarrow> ?b x \<in> elts (?B x)) \<Longrightarrow> VLambda ?A ?b \<in> elts (VPi ?A ?B)
f \<in> elts (VPi A B)

goal (1 subgoal):
 1. VLambda A (app f) \<in> elts (VPi A B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VLambda A (app f) \<in> elts (VPi A B)

goal (1 subgoal):
 1. \<And>x. x \<in> elts A \<Longrightarrow> app (VLambda A (app f)) x = app f x
[PROOF STEP]
qed auto


[STATEMENT]
lemma fst_pairs_VLambda: "fst ` pairs (VLambda A f) = elts A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` pairs (VLambda A f) = elts A
[PROOF STEP]
by (force simp: VLambda_def pairs_def)


[STATEMENT]
lemma snd_pairs_VLambda: "snd ` pairs (VLambda A f) = f ` elts A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` pairs (VLambda A f) = f ` elts A
[PROOF STEP]
by (force simp: VLambda_def pairs_def)


[STATEMENT]
lemma VLambda_eq_D1: "VLambda A f = VLambda B g \<Longrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda A f = VLambda B g \<Longrightarrow> A = B
[PROOF STEP]
by (metis ZFC_in_HOL.ext fst_pairs_VLambda)


[STATEMENT]
lemma VLambda_eq_D2: "\<lbrakk>VLambda A f = VLambda A g; x \<in> elts A\<rbrakk> \<Longrightarrow> f x = g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>VLambda A f = VLambda A g; x \<in> elts A\<rbrakk> \<Longrightarrow> f x = g x
[PROOF STEP]
by (metis beta)


[STATEMENT]
lemma TC: "TC a = a \<squnion> \<Squnion> (TC ` elts a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC a = a \<squnion> \<Squnion> (TC ` elts a)
[PROOF STEP]
by (metis (no_types, lifting) SUP_cong TC_def restrict_apply' transrec)


[STATEMENT]
lemma TC_0 [simp]: "TC 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC 0 = 0
[PROOF STEP]
by (metis TC ZFC_in_HOL.Sup_empty elts_0 image_is_empty sup_V_0_left)


[STATEMENT]
lemma arg_subset_TC: "a \<le> TC a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> TC a
[PROOF STEP]
by (metis (no_types) TC sup_ge1)


[STATEMENT]
lemma Transset_TC: "Transset(TC a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Transset (TC a)
[PROOF STEP]
proof (induction a rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Transset (TC y)) \<Longrightarrow> Transset (TC x)
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
?y \<in> elts x \<Longrightarrow> Transset (TC ?y)

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Transset (TC y)) \<Longrightarrow> Transset (TC x)
[PROOF STEP]
have 1: "v \<in> elts (TC x)" if "v \<in> elts u" "u \<in> elts x" for u v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> elts (TC x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
v \<in> elts u
u \<in> elts x

goal (1 subgoal):
 1. v \<in> elts (TC x)
[PROOF STEP]
unfolding TC [of x]
[PROOF STATE]
proof (prove)
using this:
v \<in> elts u
u \<in> elts x

goal (1 subgoal):
 1. v \<in> elts (x \<squnion> \<Squnion> (TC ` elts x))
[PROOF STEP]
using arg_subset_TC
[PROOF STATE]
proof (prove)
using this:
v \<in> elts u
u \<in> elts x
?a \<le> TC ?a

goal (1 subgoal):
 1. v \<in> elts (x \<squnion> \<Squnion> (TC ` elts x))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v \<in> elts ?u; ?u \<in> elts x\<rbrakk> \<Longrightarrow> ?v \<in> elts (TC x)

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Transset (TC y)) \<Longrightarrow> Transset (TC x)
[PROOF STEP]
have 2: "v \<in> elts (TC x)" if "v \<in> elts u" "\<exists>x\<in>elts x. u \<in> elts (TC x)" for u v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> elts (TC x)
[PROOF STEP]
using that step
[PROOF STATE]
proof (prove)
using this:
v \<in> elts u
\<exists>x\<in>elts x. u \<in> elts (TC x)
?y \<in> elts x \<Longrightarrow> Transset (TC ?y)

goal (1 subgoal):
 1. v \<in> elts (TC x)
[PROOF STEP]
unfolding TC [of x] Transset_def
[PROOF STATE]
proof (prove)
using this:
v \<in> elts u
\<exists>x\<in>elts x. u \<in> elts (TC x)
?y \<in> elts x \<Longrightarrow> \<forall>y\<in>elts (TC ?y). y \<le> TC ?y

goal (1 subgoal):
 1. v \<in> elts (x \<squnion> \<Squnion> (TC ` elts x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v \<in> elts ?u; \<exists>x\<in>elts x. ?u \<in> elts (TC x)\<rbrakk> \<Longrightarrow> ?v \<in> elts (TC x)

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Transset (TC y)) \<Longrightarrow> Transset (TC x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Transset (TC x)
[PROOF STEP]
unfolding Transset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>elts (TC x). y \<le> TC x
[PROOF STEP]
by (subst TC) (force intro: 1 2)
[PROOF STATE]
proof (state)
this:
Transset (TC x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma TC_least: "\<lbrakk>Transset x;  a\<le>x\<rbrakk> \<Longrightarrow> TC a \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Transset x; a \<le> x\<rbrakk> \<Longrightarrow> TC a \<le> x
[PROOF STEP]
proof (induction a rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>y. \<lbrakk>y \<in> elts xa; Transset x; y \<le> x\<rbrakk> \<Longrightarrow> TC y \<le> x; Transset x; xa \<le> x\<rbrakk> \<Longrightarrow> TC xa \<le> x
[PROOF STEP]
case (step y)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> elts y; Transset x; ?y \<le> x\<rbrakk> \<Longrightarrow> TC ?y \<le> x
Transset x
y \<le> x

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>y. \<lbrakk>y \<in> elts xa; Transset x; y \<le> x\<rbrakk> \<Longrightarrow> TC y \<le> x; Transset x; xa \<le> x\<rbrakk> \<Longrightarrow> TC xa \<le> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC y \<le> x
[PROOF STEP]
proof (cases "y=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = 0 \<Longrightarrow> TC y \<le> x
 2. y \<noteq> 0 \<Longrightarrow> TC y \<le> x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y = 0

goal (2 subgoals):
 1. y = 0 \<Longrightarrow> TC y \<le> x
 2. y \<noteq> 0 \<Longrightarrow> TC y \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y = 0

goal (1 subgoal):
 1. TC y \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
TC y \<le> x

goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> TC y \<le> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> TC y \<le> x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<noteq> 0

goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> TC y \<le> x
[PROOF STEP]
have "\<Squnion> (TC ` elts y) \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (TC ` elts y) \<le> x
[PROOF STEP]
proof (rule cSup_least)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. TC ` elts y \<noteq> {}
 2. \<And>xa. xa \<in> TC ` elts y \<Longrightarrow> xa \<le> x
[PROOF STEP]
show "TC ` elts y \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC ` elts y \<noteq> {}
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
y \<noteq> 0

goal (1 subgoal):
 1. TC ` elts y \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
TC ` elts y \<noteq> {}

goal (1 subgoal):
 1. \<And>xa. xa \<in> TC ` elts y \<Longrightarrow> xa \<le> x
[PROOF STEP]
show "z \<le> x" if "z \<in> TC ` elts y" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<le> x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
z \<in> TC ` elts y

goal (1 subgoal):
 1. z \<le> x
[PROOF STEP]
by (metis Transset_def image_iff step.IH step.prems vsubsetD)
[PROOF STATE]
proof (state)
this:
?z \<in> TC ` elts y \<Longrightarrow> ?z \<le> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Squnion> (TC ` elts y) \<le> x

goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> TC y \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Squnion> (TC ` elts y) \<le> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Squnion> (TC ` elts y) \<le> x

goal (1 subgoal):
 1. TC y \<le> x
[PROOF STEP]
by (simp add: step TC [of y])
[PROOF STATE]
proof (state)
this:
TC y \<le> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
TC y \<le> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_TC_imp_not_le: "x \<sqsubset> a \<Longrightarrow> \<not> a \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubset> a \<Longrightarrow> \<not> a \<le> x
[PROOF STEP]
proof (induction a arbitrary: x rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>y xa. \<lbrakk>y \<in> elts x; xa \<sqsubset> y\<rbrakk> \<Longrightarrow> \<not> y \<le> xa; xa \<sqsubset> x\<rbrakk> \<Longrightarrow> \<not> x \<le> xa
[PROOF STEP]
case (step a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> elts a; ?x \<sqsubset> ?y\<rbrakk> \<Longrightarrow> \<not> ?y \<le> ?x
x \<sqsubset> a

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>y xa. \<lbrakk>y \<in> elts x; xa \<sqsubset> y\<rbrakk> \<Longrightarrow> \<not> y \<le> xa; xa \<sqsubset> x\<rbrakk> \<Longrightarrow> \<not> x \<le> xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y \<in> elts a; ?x \<sqsubset> ?y\<rbrakk> \<Longrightarrow> \<not> ?y \<le> ?x
x \<sqsubset> a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> elts a; ?x \<sqsubset> ?y\<rbrakk> \<Longrightarrow> \<not> ?y \<le> ?x
x \<sqsubset> a

goal (1 subgoal):
 1. \<not> a \<le> x
[PROOF STEP]
unfolding TC[of a] less_TC_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> elts a; ?x \<in> elts (TC ?y)\<rbrakk> \<Longrightarrow> \<not> ?y \<le> ?x
x \<in> elts (a \<squnion> \<Squnion> (TC ` elts a))

goal (1 subgoal):
 1. \<not> a \<le> x
[PROOF STEP]
using Transset_TC Transset_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> elts a; ?x \<in> elts (TC ?y)\<rbrakk> \<Longrightarrow> \<not> ?y \<le> ?x
x \<in> elts (a \<squnion> \<Squnion> (TC ` elts a))
Transset (TC ?a)
Transset ?x \<equiv> \<forall>y\<in>elts ?x. y \<le> ?x

goal (1 subgoal):
 1. \<not> a \<le> x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<not> a \<le> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma non_TC_less_0 [iff]: "\<not> (x \<sqsubset> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x \<sqsubset> 0
[PROOF STEP]
using less_TC_imp_not_le
[PROOF STATE]
proof (prove)
using this:
?x \<sqsubset> ?a \<Longrightarrow> \<not> ?a \<le> ?x

goal (1 subgoal):
 1. \<not> x \<sqsubset> 0
[PROOF STEP]
by blast


[STATEMENT]
lemma less_TC_iff: "x \<sqsubset> y \<longleftrightarrow> (\<exists>z \<in> elts y. x \<sqsubseteq> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqsubset> y) = (\<exists>z\<in>elts y. x \<sqsubseteq> z)
[PROOF STEP]
by (auto simp: less_TC_def le_TC_def TC [of y])


[STATEMENT]
lemma nonzero_less_TC: "x \<noteq> 0 \<Longrightarrow> 0 \<sqsubset> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 \<sqsubset> x
[PROOF STEP]
by (metis eps_induct le_TC_def less_TC_iff trad_foundation)


[STATEMENT]
lemma less_irrefl_TC [simp]: "\<not> x \<sqsubset> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x \<sqsubset> x
[PROOF STEP]
using less_TC_imp_not_le
[PROOF STATE]
proof (prove)
using this:
?x \<sqsubset> ?a \<Longrightarrow> \<not> ?a \<le> ?x

goal (1 subgoal):
 1. \<not> x \<sqsubset> x
[PROOF STEP]
by blast


[STATEMENT]
lemma less_asym_TC: "\<lbrakk>x \<sqsubset> y; y \<sqsubset> x\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sqsubset> y; y \<sqsubset> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis TC_least Transset_TC Transset_def antisym_conv less_TC_def less_TC_imp_not_le order_refl)


[STATEMENT]
lemma le_antisym_TC: "\<lbrakk>x \<sqsubset> y; y \<sqsubset> x\<rbrakk> \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sqsubset> y; y \<sqsubset> x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
using less_asym_TC
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<sqsubset> ?y; ?y \<sqsubset> ?x\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>x \<sqsubset> y; y \<sqsubset> x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by blast


[STATEMENT]
lemma less_imp_le_TC [iff]: "x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
by (simp add: le_TC_def)


[STATEMENT]
lemma le_TC_refl [iff]: "x \<sqsubseteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> x
[PROOF STEP]
by (simp add: le_TC_def)


[STATEMENT]
lemma less_TC_trans [trans]: "\<lbrakk>x \<sqsubset> y; y \<sqsubset> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sqsubset> y; y \<sqsubset> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z
[PROOF STEP]
by (meson TC_least Transset_TC Transset_def less_TC_def less_eq_V_def subsetD)


[STATEMENT]
lemma less_le_TC_trans [trans]: "\<lbrakk>x \<sqsubset> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sqsubset> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z
[PROOF STEP]
using le_TC_def less_TC_trans
[PROOF STATE]
proof (prove)
using this:
?x \<sqsubseteq> ?y \<equiv> ?x \<sqsubset> ?y \<or> ?x = ?y
\<lbrakk>?x \<sqsubset> ?y; ?y \<sqsubset> ?z\<rbrakk> \<Longrightarrow> ?x \<sqsubset> ?z

goal (1 subgoal):
 1. \<lbrakk>x \<sqsubset> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z
[PROOF STEP]
by blast


[STATEMENT]
lemma le_less_TC_trans [trans]: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubset> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sqsubseteq> y; y \<sqsubset> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z
[PROOF STEP]
using le_TC_def less_TC_trans
[PROOF STATE]
proof (prove)
using this:
?x \<sqsubseteq> ?y \<equiv> ?x \<sqsubset> ?y \<or> ?x = ?y
\<lbrakk>?x \<sqsubset> ?y; ?y \<sqsubset> ?z\<rbrakk> \<Longrightarrow> ?x \<sqsubset> ?z

goal (1 subgoal):
 1. \<lbrakk>x \<sqsubseteq> y; y \<sqsubset> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z
[PROOF STEP]
by blast


[STATEMENT]
lemma le_TC_trans [trans]: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z
[PROOF STEP]
using le_TC_def le_less_TC_trans
[PROOF STATE]
proof (prove)
using this:
?x \<sqsubseteq> ?y \<equiv> ?x \<sqsubset> ?y \<or> ?x = ?y
\<lbrakk>?x \<sqsubseteq> ?y; ?y \<sqsubset> ?z\<rbrakk> \<Longrightarrow> ?x \<sqsubset> ?z

goal (1 subgoal):
 1. \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z
[PROOF STEP]
by blast


[STATEMENT]
lemma TC_sup_distrib: "TC (x \<squnion> y) = TC x \<squnion> TC y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC (x \<squnion> y) = TC x \<squnion> TC y
[PROOF STEP]
by (simp add: Sup_Un_distrib TC [of "x \<squnion> y"] TC [of x] TC [of y] image_Un sup.assoc sup_left_commute)


[STATEMENT]
lemma TC_Sup_distrib:
  assumes "small X" shows "TC (\<Squnion>X) = \<Squnion>(TC ` X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
have "\<Squnion>X \<le> \<Squnion> (TC ` X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> X \<le> \<Squnion> (TC ` X)
[PROOF STEP]
using arg_subset_TC
[PROOF STATE]
proof (prove)
using this:
?a \<le> TC ?a

goal (1 subgoal):
 1. \<Squnion> X \<le> \<Squnion> (TC ` X)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<Squnion> X \<le> \<Squnion> (TC ` X)

goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Squnion> X \<le> \<Squnion> (TC ` X)

goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
have "\<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
small X

goal (1 subgoal):
 1. \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)
[PROOF STEP]
by clarsimp (meson TC_least Transset_TC Transset_def arg_subset_TC replacement vsubsetD)
[PROOF STATE]
proof (state)
this:
\<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)

goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Squnion> X \<le> \<Squnion> (TC ` X)
\<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)
[PROOF STEP]
have "\<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)"
[PROOF STATE]
proof (prove)
using this:
\<Squnion> X \<le> \<Squnion> (TC ` X)
\<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)

goal (1 subgoal):
 1. \<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)

goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)

goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
have "\<Squnion> (TC ` X) \<le> \<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (TC ` X) \<le> \<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x)
[PROOF STEP]
proof (clarsimp simp add: Sup_le_iff assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> X; xa \<in> elts (TC x); \<forall>x\<in>X. \<forall>x\<in>elts x. xa \<notin> elts (TC x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X. xa \<in> elts x
[PROOF STEP]
show "\<exists>x\<in>X. y \<in> elts x"
      if "x \<in> X" "y \<in> elts (TC x)" "\<forall>x\<in>X. \<forall>u\<in>elts x. y \<notin> elts (TC u)" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>X. y \<in> elts x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> elts (TC x)
\<forall>x\<in>X. \<forall>u\<in>elts x. y \<notin> elts (TC u)

goal (1 subgoal):
 1. \<exists>x\<in>X. y \<in> elts x
[PROOF STEP]
by (auto simp: TC [of x])
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> X; ?y \<in> elts (TC ?x); \<forall>x\<in>X. \<forall>u\<in>elts x. ?y \<notin> elts (TC u)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X. ?y \<in> elts x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Squnion> (TC ` X) \<le> \<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x)

goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)
\<Squnion> (TC ` X) \<le> \<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)
\<Squnion> (TC ` X) \<le> \<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x)

goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
using Sup_Un_distrib TC [of "\<Squnion>X"] image_Union assms
[PROOF STATE]
proof (prove)
using this:
\<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)
\<Squnion> (TC ` X) \<le> \<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x)
\<lbrakk>small ?A; small ?B\<rbrakk> \<Longrightarrow> \<Squnion> (?A \<union> ?B) = \<Squnion> ?A \<squnion> \<Squnion> ?B
TC (\<Squnion> X) = \<Squnion> X \<squnion> \<Squnion> (TC ` elts (\<Squnion> X))
?f ` \<Union> ?S = \<Union> ((`) ?f ` ?S)
small X

goal (1 subgoal):
 1. TC (\<Squnion> X) = \<Squnion> (TC ` X)
[PROOF STEP]
by (simp add: image_Union inf_sup_aci(5) sup.absorb_iff2)
[PROOF STATE]
proof (state)
this:
TC (\<Squnion> X) = \<Squnion> (TC ` X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma TC': "TC x = x \<squnion> TC (\<Squnion> (elts x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC x = x \<squnion> TC (\<Squnion> elts x)
[PROOF STEP]
by (simp add: TC [of x] TC_Sup_distrib)


[STATEMENT]
lemma TC_eq_0_iff [simp]: "TC x = 0 \<longleftrightarrow> x=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (TC x = 0) = (x = 0)
[PROOF STEP]
using arg_subset_TC
[PROOF STATE]
proof (prove)
using this:
?a \<le> TC ?a

goal (1 subgoal):
 1. (TC x = 0) = (x = 0)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma TC_induct_down_lemma:
  assumes ab: "a \<sqsubset> b" and base: "b \<le> d"
      and step: "\<And>y z. \<lbrakk>y \<sqsubset> b; y \<in> elts d; z \<in> elts y\<rbrakk> \<Longrightarrow> z \<in> elts d"
    shows "a \<in> elts d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> elts d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> elts d
[PROOF STEP]
have "Transset (TC b \<sqinter> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Transset (TC b \<sqinter> d)
[PROOF STEP]
using Transset_TC
[PROOF STATE]
proof (prove)
using this:
Transset (TC ?a)

goal (1 subgoal):
 1. Transset (TC b \<sqinter> d)
[PROOF STEP]
unfolding Transset_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>elts (TC ?a). y \<le> TC ?a

goal (1 subgoal):
 1. \<forall>y\<in>elts (TC b \<sqinter> d). y \<le> TC b \<sqinter> d
[PROOF STEP]
by (metis inf.bounded_iff less_TC_def less_eq_V_def local.step subsetI vsubsetD)
[PROOF STATE]
proof (state)
this:
Transset (TC b \<sqinter> d)

goal (1 subgoal):
 1. a \<in> elts d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Transset (TC b \<sqinter> d)

goal (1 subgoal):
 1. a \<in> elts d
[PROOF STEP]
have "b \<le> TC b \<sqinter> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> TC b \<sqinter> d
[PROOF STEP]
by (simp add: arg_subset_TC base)
[PROOF STATE]
proof (state)
this:
b \<le> TC b \<sqinter> d

goal (1 subgoal):
 1. a \<in> elts d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Transset (TC b \<sqinter> d)
b \<le> TC b \<sqinter> d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Transset (TC b \<sqinter> d)
b \<le> TC b \<sqinter> d

goal (1 subgoal):
 1. a \<in> elts d
[PROOF STEP]
using TC_least [THEN vsubsetD] ab
[PROOF STATE]
proof (prove)
using this:
Transset (TC b \<sqinter> d)
b \<le> TC b \<sqinter> d
\<lbrakk>Transset ?b; ?a1 \<le> ?b; ?c \<in> elts (TC ?a1)\<rbrakk> \<Longrightarrow> ?c \<in> elts ?b
a \<sqsubset> b

goal (1 subgoal):
 1. a \<in> elts d
[PROOF STEP]
unfolding less_TC_def
[PROOF STATE]
proof (prove)
using this:
Transset (TC b \<sqinter> d)
b \<le> TC b \<sqinter> d
\<lbrakk>Transset ?b; ?a1 \<le> ?b; ?c \<in> elts (TC ?a1)\<rbrakk> \<Longrightarrow> ?c \<in> elts ?b
a \<in> elts (TC b)

goal (1 subgoal):
 1. a \<in> elts d
[PROOF STEP]
by (meson TC_least le_inf_iff vsubsetD)
[PROOF STATE]
proof (state)
this:
a \<in> elts d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma TC_induct_down [consumes 1, case_names base step small]:
  assumes "a \<sqsubset> b"
    and "\<And>y. y \<in> elts b \<Longrightarrow> P y"
    and "\<And>y z. \<lbrakk>y \<sqsubset> b; P y; z \<in> elts y\<rbrakk> \<Longrightarrow> P z"
    and "small (Collect P)"
  shows "P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P a
[PROOF STEP]
using TC_induct_down_lemma [of a b "set (Collect P)"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<sqsubset> b; b \<le> set (Collect P); \<And>y z. \<lbrakk>y \<sqsubset> b; y \<in> elts (set (Collect P)); z \<in> elts y\<rbrakk> \<Longrightarrow> z \<in> elts (set (Collect P))\<rbrakk> \<Longrightarrow> a \<in> elts (set (Collect P))
a \<sqsubset> b
?y \<in> elts b \<Longrightarrow> P ?y
\<lbrakk>?y \<sqsubset> b; P ?y; ?z \<in> elts ?y\<rbrakk> \<Longrightarrow> P ?z
small (Collect P)

goal (1 subgoal):
 1. P a
[PROOF STEP]
by (metis elts_of_set mem_Collect_eq vsubsetI)


[STATEMENT]
lemma rank: "rank a = set(\<Union>y \<in> elts a. elts (succ(rank y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank a = set (\<Union>y\<in>elts a. elts (ZFC_in_HOL.succ (rank y)))
[PROOF STEP]
by (subst rank_def [THEN def_transrec], simp)


[STATEMENT]
lemma rank_Sup: "rank a = \<Squnion>((\<lambda>y. succ(rank y)) ` elts a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank a = (\<Squnion>y\<in>elts a. ZFC_in_HOL.succ (rank y))
[PROOF STEP]
by (metis elts_Sup image_image rank replacement set_of_elts small_elts)


[STATEMENT]
lemma Ord_rank [simp]: "Ord(rank a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (rank a)
[PROOF STEP]
proof (induction a rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Ord (rank y)) \<Longrightarrow> Ord (rank x)
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
?y \<in> elts x \<Longrightarrow> Ord (rank ?y)

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Ord (rank y)) \<Longrightarrow> Ord (rank x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?y \<in> elts x \<Longrightarrow> Ord (rank ?y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?y \<in> elts x \<Longrightarrow> Ord (rank ?y)

goal (1 subgoal):
 1. Ord (rank x)
[PROOF STEP]
unfolding rank_Sup [of x]
[PROOF STATE]
proof (prove)
using this:
?y \<in> elts x \<Longrightarrow> Ord (rank ?y)

goal (1 subgoal):
 1. Ord (\<Squnion>y\<in>elts x. ZFC_in_HOL.succ (rank y))
[PROOF STEP]
by (metis (mono_tags, lifting) Ord_Sup Ord_succ imageE)
[PROOF STATE]
proof (state)
this:
Ord (rank x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_of_Ord: "Ord i \<Longrightarrow> rank i = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord i \<Longrightarrow> rank i = i
[PROOF STEP]
by (induction rule: Ord_induct) (metis (no_types, lifting) Ord_equality SUP_cong rank_Sup)


[STATEMENT]
lemma Ord_iff_rank: "Ord x \<longleftrightarrow> rank x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord x = (rank x = x)
[PROOF STEP]
using Ord_rank [of x] rank_of_Ord
[PROOF STATE]
proof (prove)
using this:
Ord (rank x)
Ord ?i \<Longrightarrow> rank ?i = ?i

goal (1 subgoal):
 1. Ord x = (rank x = x)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma rank_lt: "a \<in> elts b \<Longrightarrow> rank a < rank b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> elts b \<Longrightarrow> rank a < rank b
[PROOF STEP]
by (metis Ord_linear2 Ord_rank ZFC_in_HOL.SUP_le_iff rank_Sup replacement small_elts succ_le_iff order.irrefl)


[STATEMENT]
lemma rank_0 [simp]: "rank 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank 0 = 0
[PROOF STEP]
using transrec Ord_0 rank_def rank_of_Ord
[PROOF STATE]
proof (prove)
using this:
transrec ?H ?a = ?H (restrict (transrec ?H) (elts ?a)) ?a
Ord 0
rank ?a \<equiv> transrec (\<lambda>f x. set (\<Union>y\<in>elts x. elts (ZFC_in_HOL.succ (f y)))) ?a
Ord ?i \<Longrightarrow> rank ?i = ?i

goal (1 subgoal):
 1. rank 0 = 0
[PROOF STEP]
by presburger


[STATEMENT]
lemma rank_succ [simp]: "rank(succ x) = succ(rank x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank (ZFC_in_HOL.succ x) = ZFC_in_HOL.succ (rank x)
[PROOF STEP]
proof (rule order_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rank (ZFC_in_HOL.succ x) \<le> ZFC_in_HOL.succ (rank x)
 2. ZFC_in_HOL.succ (rank x) \<le> rank (ZFC_in_HOL.succ x)
[PROOF STEP]
show "rank (succ x) \<le> succ (rank x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank (ZFC_in_HOL.succ x) \<le> ZFC_in_HOL.succ (rank x)
[PROOF STEP]
by (metis (no_types, lifting) Sup_insert elts_of_set elts_succ image_insert rank small_UN small_elts subset_insertI sup.orderE vsubsetI)
[PROOF STATE]
proof (state)
this:
rank (ZFC_in_HOL.succ x) \<le> ZFC_in_HOL.succ (rank x)

goal (1 subgoal):
 1. ZFC_in_HOL.succ (rank x) \<le> rank (ZFC_in_HOL.succ x)
[PROOF STEP]
show "succ (rank x) \<le> rank (succ x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ (rank x) \<le> rank (ZFC_in_HOL.succ x)
[PROOF STEP]
by (metis (mono_tags, lifting) ZFC_in_HOL.Sup_upper elts_succ image_insert insertI1 rank_Sup replacement small_elts)
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.succ (rank x) \<le> rank (ZFC_in_HOL.succ x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_mono: "a \<le> b \<Longrightarrow> rank a \<le> rank b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> rank a \<le> rank b
[PROOF STEP]
using rank [of a] rank [of b] small_UN
[PROOF STATE]
proof (prove)
using this:
rank a = set (\<Union>y\<in>elts a. elts (ZFC_in_HOL.succ (rank y)))
rank b = set (\<Union>y\<in>elts b. elts (ZFC_in_HOL.succ (rank y)))
\<lbrakk>small ?A; \<And>x. x \<in> ?A \<Longrightarrow> small (?B x)\<rbrakk> \<Longrightarrow> small (\<Union> (?B ` ?A))

goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> rank a \<le> rank b
[PROOF STEP]
by force


[STATEMENT]
lemma VsetI: "rank b \<sqsubset> i \<Longrightarrow> b \<in> elts (Vset i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank b \<sqsubset> i \<Longrightarrow> b \<in> elts (Vset i)
[PROOF STEP]
proof (induction i arbitrary: b rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>y b. \<lbrakk>y \<in> elts x; rank b \<sqsubset> y\<rbrakk> \<Longrightarrow> b \<in> elts (Vset y); rank b \<sqsubset> x\<rbrakk> \<Longrightarrow> b \<in> elts (Vset x)
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> elts x; rank ?b \<sqsubset> ?y\<rbrakk> \<Longrightarrow> ?b \<in> elts (Vset ?y)
rank b \<sqsubset> x

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>y b. \<lbrakk>y \<in> elts x; rank b \<sqsubset> y\<rbrakk> \<Longrightarrow> b \<in> elts (Vset y); rank b \<sqsubset> x\<rbrakk> \<Longrightarrow> b \<in> elts (Vset x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y \<in> elts x; rank ?b \<sqsubset> ?y\<rbrakk> \<Longrightarrow> ?b \<in> elts (Vset ?y)
rank b \<sqsubset> x
[PROOF STEP]
consider "rank b \<in> elts x" | "(\<exists>y\<in>elts x. rank b \<in> elts (TC y))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> elts x; rank ?b \<sqsubset> ?y\<rbrakk> \<Longrightarrow> ?b \<in> elts (Vset ?y)
rank b \<sqsubset> x

goal (1 subgoal):
 1. \<lbrakk>rank b \<in> elts x \<Longrightarrow> thesis; \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using le_TC_def less_TC_def less_TC_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> elts x; rank ?b \<sqsubset> ?y\<rbrakk> \<Longrightarrow> ?b \<in> elts (Vset ?y)
rank b \<sqsubset> x
?x \<sqsubseteq> ?y \<equiv> ?x \<sqsubset> ?y \<or> ?x = ?y
?x \<sqsubset> ?y \<equiv> ?x \<in> elts (TC ?y)
(?x \<sqsubset> ?y) = (\<exists>z\<in>elts ?y. ?x \<sqsubseteq> z)

goal (1 subgoal):
 1. \<lbrakk>rank b \<in> elts x \<Longrightarrow> thesis; \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>rank b \<in> elts x \<Longrightarrow> ?thesis; \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>y b. \<lbrakk>y \<in> elts x; rank b \<sqsubset> y\<rbrakk> \<Longrightarrow> b \<in> elts (Vset y); rank b \<sqsubset> x\<rbrakk> \<Longrightarrow> b \<in> elts (Vset x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>rank b \<in> elts x \<Longrightarrow> ?thesis; \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have "\<exists>y\<in>elts x. b \<le> Vset y"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rank b \<in> elts x \<Longrightarrow> ?thesis; \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rank b \<in> elts x \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
 2. \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
rank b \<in> elts x

goal (2 subgoals):
 1. rank b \<in> elts x \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
 2. \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rank b \<in> elts x
[PROOF STEP]
have "b \<le> Vset (rank b)"
[PROOF STATE]
proof (prove)
using this:
rank b \<in> elts x

goal (1 subgoal):
 1. b \<le> Vset (rank b)
[PROOF STEP]
unfolding less_eq_V_def subset_iff
[PROOF STATE]
proof (prove)
using this:
rank b \<in> elts x

goal (1 subgoal):
 1. \<forall>t. t \<in> elts b \<longrightarrow> t \<in> elts (Vset (rank b))
[PROOF STEP]
by (meson Ord_mem_iff_lt Ord_rank le_TC_refl less_TC_iff rank_lt step.IH)
[PROOF STATE]
proof (state)
this:
b \<le> Vset (rank b)

goal (2 subgoals):
 1. rank b \<in> elts x \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
 2. \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<le> Vset (rank b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<le> Vset (rank b)

goal (1 subgoal):
 1. \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
using "1"
[PROOF STATE]
proof (prove)
using this:
b \<le> Vset (rank b)
rank b \<in> elts x

goal (1 subgoal):
 1. \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>elts x. b \<le> Vset y

goal (1 subgoal):
 1. \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>elts x. rank b \<in> elts (TC y)

goal (1 subgoal):
 1. \<exists>y\<in>elts x. rank b \<in> elts (TC y) \<Longrightarrow> \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>elts x. rank b \<in> elts (TC y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>elts x. rank b \<in> elts (TC y)

goal (1 subgoal):
 1. \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>elts x. rank b \<in> elts (TC y)
\<lbrakk>?y \<in> elts x; rank ?b \<sqsubset> ?y\<rbrakk> \<Longrightarrow> ?b \<in> elts (Vset ?y)

goal (1 subgoal):
 1. \<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
unfolding less_eq_V_def subset_iff less_TC_def
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>elts x. rank b \<in> elts (TC y)
\<lbrakk>?y \<in> elts x; rank ?b \<in> elts (TC ?y)\<rbrakk> \<Longrightarrow> ?b \<in> elts (Vset ?y)

goal (1 subgoal):
 1. \<exists>y\<in>elts x. \<forall>t. t \<in> elts b \<longrightarrow> t \<in> elts (Vset y)
[PROOF STEP]
by (meson Ord_mem_iff_lt Ord_rank Transset_TC Transset_def rank_lt vsubsetD)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>elts x. b \<le> Vset y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>elts x. b \<le> Vset y

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>y b. \<lbrakk>y \<in> elts x; rank b \<sqsubset> y\<rbrakk> \<Longrightarrow> b \<in> elts (Vset y); rank b \<sqsubset> x\<rbrakk> \<Longrightarrow> b \<in> elts (Vset x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>elts x. b \<le> Vset y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>elts x. b \<le> Vset y

goal (1 subgoal):
 1. b \<in> elts (Vset x)
[PROOF STEP]
by (simp add: Vset [of x])
[PROOF STATE]
proof (state)
this:
b \<in> elts (Vset x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ord_VsetI: "\<lbrakk>Ord i; rank b < i\<rbrakk> \<Longrightarrow> b \<in> elts (Vset i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord i; rank b < i\<rbrakk> \<Longrightarrow> b \<in> elts (Vset i)
[PROOF STEP]
by (meson Ord_mem_iff_lt Ord_rank VsetI arg_subset_TC less_TC_def vsubsetD)


[STATEMENT]
lemma arg_le_Vset_rank: "a \<le> Vset(rank a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> Vset (rank a)
[PROOF STEP]
by (simp add: Ord_VsetI rank_lt vsubsetI)


[STATEMENT]
lemma two_in_Vset:
  obtains \<alpha> where  "x \<in> elts (Vset \<alpha>)" "y \<in> elts (Vset \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>x \<in> elts (Vset \<alpha>); y \<in> elts (Vset \<alpha>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Ord_rank Ord_VsetI elts_of_set insert_iff rank_lt small_elts small_insert_iff)


[STATEMENT]
lemma rank_eq_0_iff [simp]: "rank x = 0 \<longleftrightarrow> x=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rank x = 0) = (x = 0)
[PROOF STEP]
using arg_le_Vset_rank
[PROOF STATE]
proof (prove)
using this:
?a \<le> Vset (rank ?a)

goal (1 subgoal):
 1. (rank x = 0) = (x = 0)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma small_ranks_imp_small:
  assumes "small (rank ` A)" shows "small A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small A
[PROOF STEP]
define i where "i \<equiv> set (\<Union>(elts ` (rank ` A)))"
[PROOF STATE]
proof (state)
this:
i \<equiv> set (\<Union> (elts ` rank ` A))

goal (1 subgoal):
 1. small A
[PROOF STEP]
have "Ord i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord i
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (set (\<Union> (elts ` rank ` A)))
[PROOF STEP]
using Ord_Union Ord_rank assms imageE
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> ?X \<Longrightarrow> Ord x; small ?X\<rbrakk> \<Longrightarrow> Ord (set (\<Union> (elts ` ?X)))
Ord (rank ?a)
small (rank ` A)
\<lbrakk>?b \<in> ?f ` ?A; \<And>x. \<lbrakk>?b = ?f x; x \<in> ?A\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. Ord (set (\<Union> (elts ` rank ` A)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ord i

goal (1 subgoal):
 1. small A
[PROOF STEP]
have *: "Vset (rank x) \<le> (Vset i)" if "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vset (rank x) \<le> Vset i
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vset (rank x) \<le> Vset (set (\<Union> (elts ` rank ` A)))
[PROOF STEP]
by (metis Ord_rank Sup_V_def ZFC_in_HOL.Sup_upper Vfrom_mono assms imageI le_less that)
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> Vset (rank ?x) \<le> Vset i

goal (1 subgoal):
 1. small A
[PROOF STEP]
have "A \<subseteq> elts (VPow (Vset i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> elts (VPow (Vset i))
[PROOF STEP]
by (meson "*" VPow_iff arg_le_Vset_rank order.trans subsetI)
[PROOF STATE]
proof (state)
this:
A \<subseteq> elts (VPow (Vset i))

goal (1 subgoal):
 1. small A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> elts (VPow (Vset i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> elts (VPow (Vset i))

goal (1 subgoal):
 1. small A
[PROOF STEP]
using down
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> elts (VPow (Vset i))
?Y \<subseteq> elts ?x \<Longrightarrow> small ?Y

goal (1 subgoal):
 1. small A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
small A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_Union: "rank(\<Squnion> A) = \<Squnion> (rank ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank (\<Squnion> A) = \<Squnion> (rank ` A)
[PROOF STEP]
proof (rule order_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rank (\<Squnion> A) \<le> \<Squnion> (rank ` A)
 2. \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
have "elts (\<Squnion>y\<in>elts (\<Squnion> A). succ (rank y)) \<subseteq> elts (\<Squnion> (rank ` A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (\<Squnion>y\<in>elts (\<Squnion> A). ZFC_in_HOL.succ (rank y)) \<subseteq> elts (\<Squnion> (rank ` A))
[PROOF STEP]
by clarsimp (meson Ord_mem_iff_lt Ord_rank less_V_def rank_lt vsubsetD)
[PROOF STATE]
proof (state)
this:
elts (\<Squnion>y\<in>elts (\<Squnion> A). ZFC_in_HOL.succ (rank y)) \<subseteq> elts (\<Squnion> (rank ` A))

goal (2 subgoals):
 1. rank (\<Squnion> A) \<le> \<Squnion> (rank ` A)
 2. \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (\<Squnion>y\<in>elts (\<Squnion> A). ZFC_in_HOL.succ (rank y)) \<subseteq> elts (\<Squnion> (rank ` A))
[PROOF STEP]
show "rank (\<Squnion> A) \<le> \<Squnion> (rank ` A)"
[PROOF STATE]
proof (prove)
using this:
elts (\<Squnion>y\<in>elts (\<Squnion> A). ZFC_in_HOL.succ (rank y)) \<subseteq> elts (\<Squnion> (rank ` A))

goal (1 subgoal):
 1. rank (\<Squnion> A) \<le> \<Squnion> (rank ` A)
[PROOF STEP]
by (metis less_eq_V_def rank_Sup)
[PROOF STATE]
proof (state)
this:
rank (\<Squnion> A) \<le> \<Squnion> (rank ` A)

goal (1 subgoal):
 1. \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
show "\<Squnion> (rank ` A) \<le> rank (\<Squnion> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
proof (cases "small A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. small A \<Longrightarrow> \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
 2. \<not> small A \<Longrightarrow> \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
small A

goal (2 subgoals):
 1. small A \<Longrightarrow> \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
 2. \<not> small A \<Longrightarrow> \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
small A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
small A

goal (1 subgoal):
 1. \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
by (simp add: ZFC_in_HOL.SUP_le_iff ZFC_in_HOL.Sup_upper rank_mono)
[PROOF STATE]
proof (state)
this:
\<Squnion> (rank ` A) \<le> rank (\<Squnion> A)

goal (1 subgoal):
 1. \<not> small A \<Longrightarrow> \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> small A \<Longrightarrow> \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> small A

goal (1 subgoal):
 1. \<not> small A \<Longrightarrow> \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> small A
[PROOF STEP]
have "\<not> small (rank ` A)"
[PROOF STATE]
proof (prove)
using this:
\<not> small A

goal (1 subgoal):
 1. \<not> small (rank ` A)
[PROOF STEP]
using small_ranks_imp_small
[PROOF STATE]
proof (prove)
using this:
\<not> small A
small (rank ` ?A) \<Longrightarrow> small ?A

goal (1 subgoal):
 1. \<not> small (rank ` A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> small (rank ` A)

goal (1 subgoal):
 1. \<not> small A \<Longrightarrow> \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> small (rank ` A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> small (rank ` A)

goal (1 subgoal):
 1. \<Squnion> (rank ` A) \<le> rank (\<Squnion> A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Squnion> (rank ` A) \<le> rank (\<Squnion> A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Squnion> (rank ` A) \<le> rank (\<Squnion> A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_bounded_rank:  "small {x. rank x \<in> elts a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {x. rank x \<in> elts a}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small {x. rank x \<in> elts a}
[PROOF STEP]
have "{x. rank x \<in> elts a} \<subseteq> {x. rank x \<sqsubset> a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. rank x \<in> elts a} \<subseteq> {x. rank x \<sqsubset> a}
[PROOF STEP]
using less_TC_iff
[PROOF STATE]
proof (prove)
using this:
(?x \<sqsubset> ?y) = (\<exists>z\<in>elts ?y. ?x \<sqsubseteq> z)

goal (1 subgoal):
 1. {x. rank x \<in> elts a} \<subseteq> {x. rank x \<sqsubset> a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. rank x \<in> elts a} \<subseteq> {x. rank x \<sqsubset> a}

goal (1 subgoal):
 1. small {x. rank x \<in> elts a}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x. rank x \<in> elts a} \<subseteq> {x. rank x \<sqsubset> a}

goal (1 subgoal):
 1. small {x. rank x \<in> elts a}
[PROOF STEP]
have "\<dots> \<subseteq> elts (Vset a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. rank x \<sqsubset> a} \<subseteq> elts (Vset a)
[PROOF STEP]
using VsetI
[PROOF STATE]
proof (prove)
using this:
rank ?b \<sqsubset> ?i \<Longrightarrow> ?b \<in> elts (Vset ?i)

goal (1 subgoal):
 1. {x. rank x \<sqsubset> a} \<subseteq> elts (Vset a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{x. rank x \<sqsubset> a} \<subseteq> elts (Vset a)

goal (1 subgoal):
 1. small {x. rank x \<in> elts a}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{x. rank x \<in> elts a} \<subseteq> elts (Vset a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{x. rank x \<in> elts a} \<subseteq> elts (Vset a)

goal (1 subgoal):
 1. small {x. rank x \<in> elts a}
[PROOF STEP]
using down
[PROOF STATE]
proof (prove)
using this:
{x. rank x \<in> elts a} \<subseteq> elts (Vset a)
?Y \<subseteq> elts ?x \<Longrightarrow> small ?Y

goal (1 subgoal):
 1. small {x. rank x \<in> elts a}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
small {x. rank x \<in> elts a}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_bounded_rank_le:  "small {x. rank x \<le> a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {x. rank x \<le> a}
[PROOF STEP]
using small_bounded_rank [of "VPow a"] VPow_iff [of _ a]
[PROOF STATE]
proof (prove)
using this:
small {x. rank x \<in> elts (VPow a)}
(?y \<in> elts (VPow a)) = (?y \<le> a)

goal (1 subgoal):
 1. small {x. rank x \<le> a}
[PROOF STEP]
by simp


[STATEMENT]
lemma TC_rank_lt: "a \<sqsubset> b \<Longrightarrow> rank a < rank b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqsubset> b \<Longrightarrow> rank a < rank b
[PROOF STEP]
proof (induction rule: TC_induct_down)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>y. y \<in> elts b \<Longrightarrow> rank y < rank b
 2. \<And>y z. \<lbrakk>y \<sqsubset> b; rank y < rank b; z \<in> elts y\<rbrakk> \<Longrightarrow> rank z < rank b
 3. small {a. rank a < rank b}
[PROOF STEP]
case (base y)
[PROOF STATE]
proof (state)
this:
y \<in> elts b

goal (3 subgoals):
 1. \<And>y. y \<in> elts b \<Longrightarrow> rank y < rank b
 2. \<And>y z. \<lbrakk>y \<sqsubset> b; rank y < rank b; z \<in> elts y\<rbrakk> \<Longrightarrow> rank z < rank b
 3. small {a. rank a < rank b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> elts b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
y \<in> elts b

goal (1 subgoal):
 1. rank y < rank b
[PROOF STEP]
by (simp add: rank_lt)
[PROOF STATE]
proof (state)
this:
rank y < rank b

goal (2 subgoals):
 1. \<And>y z. \<lbrakk>y \<sqsubset> b; rank y < rank b; z \<in> elts y\<rbrakk> \<Longrightarrow> rank z < rank b
 2. small {a. rank a < rank b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>y \<sqsubset> b; rank y < rank b; z \<in> elts y\<rbrakk> \<Longrightarrow> rank z < rank b
 2. small {a. rank a < rank b}
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
y \<sqsubset> b
z \<in> elts y
rank y < rank b

goal (2 subgoals):
 1. \<And>y z. \<lbrakk>y \<sqsubset> b; rank y < rank b; z \<in> elts y\<rbrakk> \<Longrightarrow> rank z < rank b
 2. small {a. rank a < rank b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<sqsubset> b
z \<in> elts y
rank y < rank b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
y \<sqsubset> b
z \<in> elts y
rank y < rank b

goal (1 subgoal):
 1. rank z < rank b
[PROOF STEP]
using less_trans rank_lt
[PROOF STATE]
proof (prove)
using this:
y \<sqsubset> b
z \<in> elts y
rank y < rank b
\<lbrakk>?x < ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z
?a \<in> elts ?b \<Longrightarrow> rank ?a < rank ?b

goal (1 subgoal):
 1. rank z < rank b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rank z < rank b

goal (1 subgoal):
 1. small {a. rank a < rank b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small {a. rank a < rank b}
[PROOF STEP]
case small
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. small {a. rank a < rank b}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {a. rank a < rank b}
[PROOF STEP]
using smaller_than_small [OF small_bounded_rank_le [of "rank b"]]
[PROOF STATE]
proof (prove)
using this:
?B \<subseteq> {x. rank x \<le> rank b} \<Longrightarrow> small ?B

goal (1 subgoal):
 1. small {a. rank a < rank b}
[PROOF STEP]
by (simp add: Collect_mono less_V_def)
[PROOF STATE]
proof (state)
this:
small {a. rank a < rank b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma TC_rank_mem: "x \<sqsubset> y \<Longrightarrow> rank x \<in> elts (rank y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubset> y \<Longrightarrow> rank x \<in> elts (rank y)
[PROOF STEP]
by (simp add: Ord_mem_iff_lt TC_rank_lt)


[STATEMENT]
lemma wf_TC_less: "wf {(x,y). x \<sqsubset> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(x, y). x \<sqsubset> y}
[PROOF STEP]
proof (rule wf_subset [OF wf_inv_image [OF foundation, of rank]])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(x, y). x \<sqsubset> y} \<subseteq> inv_image {(x, y). x \<in> elts y} rank
[PROOF STEP]
show "{(x, y). x \<sqsubset> y} \<subseteq> inv_image {(x, y). x \<in> elts y} rank"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<sqsubset> y} \<subseteq> inv_image {(x, y). x \<in> elts y} rank
[PROOF STEP]
by (auto simp: TC_rank_mem inv_image_def)
[PROOF STATE]
proof (state)
this:
{(x, y). x \<sqsubset> y} \<subseteq> inv_image {(x, y). x \<in> elts y} rank

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_TC_minimal:
  assumes "P a"
  obtains x where "P x" "x \<sqsubseteq> a" "\<And>y. y \<sqsubset> x \<Longrightarrow> \<not> P y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>P x; x \<sqsubseteq> a; \<And>y. y \<sqsubset> x \<Longrightarrow> \<not> P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfE_min' [OF wf_TC_less, of "{x. P x \<and> x \<sqsubseteq> a}"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{x. P x \<and> x \<sqsubseteq> a} \<noteq> {}; \<And>z. \<lbrakk>z \<in> {x. P x \<and> x \<sqsubseteq> a}; \<And>y. (y, z) \<in> {(x, y). x \<sqsubset> y} \<Longrightarrow> y \<notin> {x. P x \<and> x \<sqsubseteq> a}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>P x; x \<sqsubseteq> a; \<And>y. y \<sqsubset> x \<Longrightarrow> \<not> P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp (metis le_TC_def less_le_TC_trans assms)


[STATEMENT]
lemma Vfrom_rank_eq: "Vfrom A (rank(x)) = Vfrom A x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A (rank x) = Vfrom A x
[PROOF STEP]
proof (rule order_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Vfrom A (rank x) \<le> Vfrom A x
 2. Vfrom A x \<le> Vfrom A (rank x)
[PROOF STEP]
show "Vfrom A (rank x) \<le> Vfrom A x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A (rank x) \<le> Vfrom A x
[PROOF STEP]
proof (induction x rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Vfrom A (rank y) \<le> Vfrom A y) \<Longrightarrow> Vfrom A (rank x) \<le> Vfrom A x
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
?y \<in> elts x \<Longrightarrow> Vfrom A (rank ?y) \<le> Vfrom A ?y

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Vfrom A (rank y) \<le> Vfrom A y) \<Longrightarrow> Vfrom A (rank x) \<le> Vfrom A x
[PROOF STEP]
have "(\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts x. VPow (Vfrom A j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts x. VPow (Vfrom A j))
[PROOF STEP]
apply (rule Sup_least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>j. VPow (Vfrom A j)) ` elts (rank x) \<Longrightarrow> x \<le> (\<Squnion>j\<in>elts x. VPow (Vfrom A j))
[PROOF STEP]
apply (clarsimp simp add: rank [of x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xaa xb xc. \<lbrakk>xaa \<le> Vfrom A xb; xc \<in> elts x; xb = rank xc \<or> xb \<in> elts (rank xc)\<rbrakk> \<Longrightarrow> \<exists>x\<in>elts x. xaa \<le> Vfrom A x
[PROOF STEP]
by (meson Ord_in_Ord Ord_rank OrdmemD Vfrom_mono order.trans less_imp_le order.refl step)
[PROOF STATE]
proof (state)
this:
(\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts x. VPow (Vfrom A j))

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Vfrom A (rank y) \<le> Vfrom A y) \<Longrightarrow> Vfrom A (rank x) \<le> Vfrom A x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts x. VPow (Vfrom A j))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts x. VPow (Vfrom A j))

goal (1 subgoal):
 1. Vfrom A (rank x) \<le> Vfrom A x
[PROOF STEP]
by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2)
[PROOF STATE]
proof (state)
this:
Vfrom A (rank x) \<le> Vfrom A x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Vfrom A (rank x) \<le> Vfrom A x

goal (1 subgoal):
 1. Vfrom A x \<le> Vfrom A (rank x)
[PROOF STEP]
show "Vfrom A x \<le> Vfrom A (rank x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A x \<le> Vfrom A (rank x)
[PROOF STEP]
proof (induction x rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Vfrom A y \<le> Vfrom A (rank y)) \<Longrightarrow> Vfrom A x \<le> Vfrom A (rank x)
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
?y \<in> elts x \<Longrightarrow> Vfrom A ?y \<le> Vfrom A (rank ?y)

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Vfrom A y \<le> Vfrom A (rank y)) \<Longrightarrow> Vfrom A x \<le> Vfrom A (rank x)
[PROOF STEP]
have "(\<Squnion>j\<in>elts x. VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>j\<in>elts x. VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j))
[PROOF STEP]
using step.IH TC_rank_mem less_TC_iff
[PROOF STATE]
proof (prove)
using this:
?y \<in> elts x \<Longrightarrow> Vfrom A ?y \<le> Vfrom A (rank ?y)
?x \<sqsubset> ?y \<Longrightarrow> rank ?x \<in> elts (rank ?y)
(?x \<sqsubset> ?y) = (\<exists>z\<in>elts ?y. ?x \<sqsubseteq> z)

goal (1 subgoal):
 1. (\<Squnion>j\<in>elts x. VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Squnion>j\<in>elts x. VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j))

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> Vfrom A y \<le> Vfrom A (rank y)) \<Longrightarrow> Vfrom A x \<le> Vfrom A (rank x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Squnion>j\<in>elts x. VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>j\<in>elts x. VPow (Vfrom A j)) \<le> (\<Squnion>j\<in>elts (rank x). VPow (Vfrom A j))

goal (1 subgoal):
 1. Vfrom A x \<le> Vfrom A (rank x)
[PROOF STEP]
by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2)
[PROOF STATE]
proof (state)
this:
Vfrom A x \<le> Vfrom A (rank x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Vfrom A x \<le> Vfrom A (rank x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Vfrom_succ: "Vfrom A (succ(i)) = A \<squnion> VPow(Vfrom A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A (ZFC_in_HOL.succ i) = A \<squnion> VPow (Vfrom A i)
[PROOF STEP]
by (metis Ord_rank Vfrom_rank_eq Vfrom_succ_Ord rank_succ)


[STATEMENT]
lemma Vset_succ_TC:
  assumes "x \<in> elts (Vset (ZFC_in_HOL.succ k))" "u \<sqsubset> x"
  shows "u \<in> elts (Vset k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> elts (Vset k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> elts (Vset (ZFC_in_HOL.succ k))
u \<sqsubset> x

goal (1 subgoal):
 1. u \<in> elts (Vset k)
[PROOF STEP]
using TC_least Transset_Vfrom Vfrom_succ less_TC_def
[PROOF STATE]
proof (prove)
using this:
x \<in> elts (Vset (ZFC_in_HOL.succ k))
u \<sqsubset> x
\<lbrakk>Transset ?x; ?a \<le> ?x\<rbrakk> \<Longrightarrow> TC ?a \<le> ?x
Transset ?A \<Longrightarrow> Transset (Vfrom ?A ?i)
Vfrom ?A (ZFC_in_HOL.succ ?i) = ?A \<squnion> VPow (Vfrom ?A ?i)
?x \<sqsubset> ?y \<equiv> ?x \<in> elts (TC ?y)

goal (1 subgoal):
 1. u \<in> elts (Vset k)
[PROOF STEP]
by auto


[STATEMENT]
lemma VWO: "{(x,y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV
[PROOF STEP]
unfolding VWO_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> elts y} \<subseteq> (SOME r. {(x, y). x \<in> elts y} \<subseteq> r \<and> Well_order r \<and> Field r = UNIV) \<and> Well_order (SOME r. {(x, y). x \<in> elts y} \<subseteq> r \<and> Well_order r \<and> Field r = UNIV) \<and> Field (SOME r. {(x, y). x \<in> elts y} \<subseteq> r \<and> Well_order r \<and> Field r = UNIV) = UNIV
[PROOF STEP]
by (metis (mono_tags, lifting) VWO_def foundation someI_ex total_well_order_extension)


[STATEMENT]
lemma wf_VWO: "wf(VWO - Id)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (VWO - Id)
[PROOF STEP]
using VWO well_order_on_def
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV
well_order_on ?A ?r \<equiv> linear_order_on ?A ?r \<and> wf (?r - Id)

goal (1 subgoal):
 1. wf (VWO - Id)
[PROOF STEP]
by blast


[STATEMENT]
lemma wf_Ord_less: "wf {(x, y). Ord y \<and> x < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(x, y). Ord y \<and> x < y}
[PROOF STEP]
by (metis (no_types, lifting) Ord_mem_iff_lt eps_induct wfPUNIVI wfP_def)


[STATEMENT]
lemma refl_VWO: "refl VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl VWO
[PROOF STEP]
using VWO order_on_defs
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV
preorder_on ?A ?r \<equiv> refl_on ?A ?r \<and> trans ?r
partial_order_on ?A ?r \<equiv> preorder_on ?A ?r \<and> antisym ?r
linear_order_on ?A ?r \<equiv> partial_order_on ?A ?r \<and> total_on ?A ?r
strict_linear_order_on ?A ?r \<equiv> trans ?r \<and> irrefl ?r \<and> total_on ?A ?r
well_order_on ?A ?r \<equiv> linear_order_on ?A ?r \<and> wf (?r - Id)

goal (1 subgoal):
 1. refl VWO
[PROOF STEP]
by fastforce


[STATEMENT]
lemma trans_VWO: "trans VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans VWO
[PROOF STEP]
using VWO
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV

goal (1 subgoal):
 1. trans VWO
[PROOF STEP]
by (simp add: VWO wo_rel.TRANS wo_rel_def)


[STATEMENT]
lemma antisym_VWO: "antisym VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisym VWO
[PROOF STEP]
using VWO
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV

goal (1 subgoal):
 1. antisym VWO
[PROOF STEP]
by (simp add: VWO wo_rel.ANTISYM wo_rel_def)


[STATEMENT]
lemma total_VWO: "total VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total VWO
[PROOF STEP]
using VWO
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV

goal (1 subgoal):
 1. total VWO
[PROOF STEP]
by (metis wo_rel.TOTAL wo_rel.intro)


[STATEMENT]
lemma total_VWOId: "total (VWO-Id)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total (VWO - Id)
[PROOF STEP]
by (simp add: total_VWO)


[STATEMENT]
lemma Linear_order_VWO: "Linear_order VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order VWO
[PROOF STEP]
using VWO well_order_on_def
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV
well_order_on ?A ?r \<equiv> linear_order_on ?A ?r \<and> wf (?r - Id)

goal (1 subgoal):
 1. Linear_order VWO
[PROOF STEP]
by blast


[STATEMENT]
lemma wo_rel_VWO: "wo_rel VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wo_rel VWO
[PROOF STEP]
using VWO wo_rel_def
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV
wo_rel ?r \<equiv> Well_order ?r

goal (1 subgoal):
 1. wo_rel VWO
[PROOF STEP]
by blast


[STATEMENT]
lemma mem_imp_VWO: "x \<in> elts y \<Longrightarrow> (x,y) \<in> VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> elts y \<Longrightarrow> (x, y) \<in> VWO
[PROOF STEP]
using VWO
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV

goal (1 subgoal):
 1. x \<in> elts y \<Longrightarrow> (x, y) \<in> VWO
[PROOF STEP]
by blast


[STATEMENT]
lemma less_TC_imp_VWO: "x \<sqsubset> y \<Longrightarrow> (x,y) \<in> VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubset> y \<Longrightarrow> (x, y) \<in> VWO
[PROOF STEP]
unfolding less_TC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> elts (TC y) \<Longrightarrow> (x, y) \<in> VWO
[PROOF STEP]
proof (induction y arbitrary: x rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>y xa. \<lbrakk>y \<in> elts x; xa \<in> elts (TC y)\<rbrakk> \<Longrightarrow> (xa, y) \<in> VWO; xa \<in> elts (TC x)\<rbrakk> \<Longrightarrow> (xa, x) \<in> VWO
[PROOF STEP]
case (step y' u)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> elts y'; ?x \<in> elts (TC ?y)\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> VWO
u \<in> elts (TC y')

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>y xa. \<lbrakk>y \<in> elts x; xa \<in> elts (TC y)\<rbrakk> \<Longrightarrow> (xa, y) \<in> VWO; xa \<in> elts (TC x)\<rbrakk> \<Longrightarrow> (xa, x) \<in> VWO
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y \<in> elts y'; ?x \<in> elts (TC ?y)\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> VWO
u \<in> elts (TC y')
[PROOF STEP]
consider "u \<in> elts y'" | v where "v \<in> elts y'" "u \<in> elts (TC v)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> elts y'; ?x \<in> elts (TC ?y)\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> VWO
u \<in> elts (TC y')

goal (1 subgoal):
 1. \<lbrakk>u \<in> elts y' \<Longrightarrow> thesis; \<And>v. \<lbrakk>v \<in> elts y'; u \<in> elts (TC v)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: TC [of y'])
[PROOF STATE]
proof (state)
this:
\<lbrakk>u \<in> elts y' \<Longrightarrow> ?thesis; \<And>v. \<lbrakk>v \<in> elts y'; u \<in> elts (TC v)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>y xa. \<lbrakk>y \<in> elts x; xa \<in> elts (TC y)\<rbrakk> \<Longrightarrow> (xa, y) \<in> VWO; xa \<in> elts (TC x)\<rbrakk> \<Longrightarrow> (xa, x) \<in> VWO
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>u \<in> elts y' \<Longrightarrow> ?thesis; \<And>v. \<lbrakk>v \<in> elts y'; u \<in> elts (TC v)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<in> elts y' \<Longrightarrow> ?thesis; \<And>v. \<lbrakk>v \<in> elts y'; u \<in> elts (TC v)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (u, y') \<in> VWO
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<in> elts y' \<Longrightarrow> (u, y') \<in> VWO
 2. \<And>v. \<lbrakk>v \<in> elts y'; u \<in> elts (TC v)\<rbrakk> \<Longrightarrow> (u, y') \<in> VWO
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
v \<in> elts y'
u \<in> elts (TC v)

goal (2 subgoals):
 1. u \<in> elts y' \<Longrightarrow> (u, y') \<in> VWO
 2. \<And>v. \<lbrakk>v \<in> elts y'; u \<in> elts (TC v)\<rbrakk> \<Longrightarrow> (u, y') \<in> VWO
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> elts y'
u \<in> elts (TC v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> elts y'
u \<in> elts (TC v)

goal (1 subgoal):
 1. (u, y') \<in> VWO
[PROOF STEP]
by (meson mem_imp_VWO step.IH transD trans_VWO)
[PROOF STATE]
proof (state)
this:
(u, y') \<in> VWO

goal (1 subgoal):
 1. u \<in> elts y' \<Longrightarrow> (u, y') \<in> VWO
[PROOF STEP]
qed (use mem_imp_VWO in blast)
[PROOF STATE]
proof (state)
this:
(u, y') \<in> VWO

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma le_TC_imp_VWO: "x \<sqsubseteq> y \<Longrightarrow> (x,y) \<in> VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> y \<Longrightarrow> (x, y) \<in> VWO
[PROOF STEP]
by (metis Diff_iff Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO le_TC_def less_TC_imp_VWO)


[STATEMENT]
lemma le_TC_0_iff [simp]: "x \<sqsubseteq> 0 \<longleftrightarrow> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqsubseteq> 0) = (x = 0)
[PROOF STEP]
by (simp add: le_TC_def)


[STATEMENT]
lemma less_TC_succ: " x \<sqsubset> succ \<beta> \<longleftrightarrow> x \<sqsubset> \<beta> \<or> x = \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqsubset> ZFC_in_HOL.succ \<beta>) = (x \<sqsubset> \<beta> \<or> x = \<beta>)
[PROOF STEP]
by (metis elts_succ insert_iff le_TC_def less_TC_iff)


[STATEMENT]
lemma le_TC_succ: "x \<sqsubseteq> succ \<beta> \<longleftrightarrow> x \<sqsubseteq> \<beta> \<or> x = succ \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqsubseteq> ZFC_in_HOL.succ \<beta>) = (x \<sqsubseteq> \<beta> \<or> x = ZFC_in_HOL.succ \<beta>)
[PROOF STEP]
by (simp add: le_TC_def less_TC_succ)


[STATEMENT]
lemma Transset_TC_eq [simp]: "Transset x \<Longrightarrow> TC x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Transset x \<Longrightarrow> TC x = x
[PROOF STEP]
by (simp add: TC_least arg_subset_TC eq_iff)


[STATEMENT]
lemma Ord_TC_less_iff: "\<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> \<beta> \<sqsubset> \<alpha> \<longleftrightarrow> \<beta> < \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> (\<beta> \<sqsubset> \<alpha>) = (\<beta> < \<alpha>)
[PROOF STEP]
by (metis Ord_def Ord_mem_iff_lt Transset_TC_eq less_TC_def)


[STATEMENT]
lemma Ord_mem_iff_less_TC: "Ord l \<Longrightarrow> k \<in> elts l \<longleftrightarrow> k \<sqsubset> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord l \<Longrightarrow> (k \<in> elts l) = (k \<sqsubset> l)
[PROOF STEP]
by (simp add: Ord_def less_TC_def)


[STATEMENT]
lemma le_TC_Ord: "\<lbrakk>\<beta> \<sqsubseteq> \<alpha>; Ord \<alpha>\<rbrakk> \<Longrightarrow> Ord \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<beta> \<sqsubseteq> \<alpha>; Ord \<alpha>\<rbrakk> \<Longrightarrow> Ord \<beta>
[PROOF STEP]
by (metis Ord_def Ord_in_Ord Transset_TC_eq le_TC_def less_TC_def)


[STATEMENT]
lemma Ord_less_TC_mem:
  assumes "Ord \<alpha>" "\<beta> \<sqsubset> \<alpha>" shows "\<beta> \<in> elts \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<beta> \<in> elts \<alpha>
[PROOF STEP]
using Ord_def assms less_TC_def
[PROOF STATE]
proof (prove)
using this:
Ord ?x \<equiv> Transset ?x \<and> (\<forall>y\<in>elts ?x. Transset y)
Ord \<alpha>
\<beta> \<sqsubset> \<alpha>
?x \<sqsubset> ?y \<equiv> ?x \<in> elts (TC ?y)

goal (1 subgoal):
 1. \<beta> \<in> elts \<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma VWO_TC_le: "\<lbrakk>Ord \<alpha>; Ord \<beta>; (\<beta>, \<alpha>) \<in> VWO\<rbrakk> \<Longrightarrow> \<beta> \<sqsubseteq> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord \<alpha>; Ord \<beta>; (\<beta>, \<alpha>) \<in> VWO\<rbrakk> \<Longrightarrow> \<beta> \<sqsubseteq> \<alpha>
[PROOF STEP]
proof (induct \<alpha> arbitrary: \<beta> rule: Ord_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x \<beta>. \<lbrakk>Ord x; \<And>y \<beta>. \<lbrakk>y \<in> elts x; Ord \<beta>; (\<beta>, y) \<in> VWO\<rbrakk> \<Longrightarrow> \<beta> \<sqsubseteq> y; Ord \<beta>; (\<beta>, x) \<in> VWO\<rbrakk> \<Longrightarrow> \<beta> \<sqsubseteq> x
[PROOF STEP]
case (step \<alpha>)
[PROOF STATE]
proof (state)
this:
Ord \<alpha>
\<lbrakk>?y \<in> elts \<alpha>; Ord ?\<beta>; (?\<beta>, ?y) \<in> VWO\<rbrakk> \<Longrightarrow> ?\<beta> \<sqsubseteq> ?y
Ord \<beta>
(\<beta>, \<alpha>) \<in> VWO

goal (1 subgoal):
 1. \<And>x \<beta>. \<lbrakk>Ord x; \<And>y \<beta>. \<lbrakk>y \<in> elts x; Ord \<beta>; (\<beta>, y) \<in> VWO\<rbrakk> \<Longrightarrow> \<beta> \<sqsubseteq> y; Ord \<beta>; (\<beta>, x) \<in> VWO\<rbrakk> \<Longrightarrow> \<beta> \<sqsubseteq> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ord \<alpha>
\<lbrakk>?y \<in> elts \<alpha>; Ord ?\<beta>; (?\<beta>, ?y) \<in> VWO\<rbrakk> \<Longrightarrow> ?\<beta> \<sqsubseteq> ?y
Ord \<beta>
(\<beta>, \<alpha>) \<in> VWO
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
\<lbrakk>?y \<in> elts \<alpha>; Ord ?\<beta>; (?\<beta>, ?y) \<in> VWO\<rbrakk> \<Longrightarrow> ?\<beta> \<sqsubseteq> ?y
Ord \<beta>
(\<beta>, \<alpha>) \<in> VWO

goal (1 subgoal):
 1. \<beta> \<sqsubseteq> \<alpha>
[PROOF STEP]
by (metis DiffI IdD Linear_order_VWO Linear_order_in_diff_Id Ord_linear Ord_mem_iff_less_TC VWO iso_tuple_UNIV_I le_TC_def mem_imp_VWO)
[PROOF STATE]
proof (state)
this:
\<beta> \<sqsubseteq> \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma VWO_iff_Ord_le [simp]: "\<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> (\<beta>, \<alpha>) \<in> VWO \<longleftrightarrow> \<beta> \<le> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> ((\<beta>, \<alpha>) \<in> VWO) = (\<beta> \<le> \<alpha>)
[PROOF STEP]
by (metis VWO_TC_le Ord_TC_less_iff le_TC_def le_TC_imp_VWO le_less)


[STATEMENT]
lemma zero_TC_le [iff]: "0 \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<sqsubseteq> y
[PROOF STEP]
using le_TC_def nonzero_less_TC
[PROOF STATE]
proof (prove)
using this:
?x \<sqsubseteq> ?y \<equiv> ?x \<sqsubset> ?y \<or> ?x = ?y
?x \<noteq> 0 \<Longrightarrow> 0 \<sqsubset> ?x

goal (1 subgoal):
 1. 0 \<sqsubseteq> y
[PROOF STEP]
by auto


[STATEMENT]
lemma succ_le_TC_iff: "Ord j \<Longrightarrow> succ i \<sqsubseteq> j \<longleftrightarrow> i \<sqsubset> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord j \<Longrightarrow> (ZFC_in_HOL.succ i \<sqsubseteq> j) = (i \<sqsubset> j)
[PROOF STEP]
by (metis Ord_in_Ord Ord_linear Ord_mem_iff_less_TC Ord_succ le_TC_def less_TC_succ less_asym_TC)


[STATEMENT]
lemma VWO_0_iff [simp]: "(x,0) \<in> VWO \<longleftrightarrow> x=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, 0) \<in> VWO) = (x = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, 0) \<in> VWO \<Longrightarrow> x = 0
 2. x = 0 \<Longrightarrow> (x, 0) \<in> VWO
[PROOF STEP]
show "x = 0" if "(x, 0) \<in> VWO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = 0
[PROOF STEP]
using zero_TC_le [of x] le_TC_imp_VWO that
[PROOF STATE]
proof (prove)
using this:
0 \<sqsubseteq> x
?x \<sqsubseteq> ?y \<Longrightarrow> (?x, ?y) \<in> VWO
(x, 0) \<in> VWO

goal (1 subgoal):
 1. x = 0
[PROOF STEP]
by (metis DiffI Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO pair_in_Id_conv)
[PROOF STATE]
proof (state)
this:
(x, 0) \<in> VWO \<Longrightarrow> x = 0

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> (x, 0) \<in> VWO
[PROOF STEP]
qed auto


[STATEMENT]
lemma VWO_antisym:
  assumes "(x,y) \<in> VWO" "(y,x) \<in> VWO" shows "x=y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis Diff_iff IdD Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO assms)


[STATEMENT]
lemma wf_VWF [iff]: "wf VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf VWF
[PROOF STEP]
by (simp add: VWF_def wf_VWO)


[STATEMENT]
lemma trans_VWF [iff]: "trans VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans VWF
[PROOF STEP]
by (simp add: VWF_def antisym_VWO trans_VWO trans_diff_Id)


[STATEMENT]
lemma asym_VWF [iff]: "asym VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asym VWF
[PROOF STEP]
by (metis VWF_def asym.intros irrefl_diff_Id wf_VWF wf_not_sym)


[STATEMENT]
lemma total_VWF [iff]: "total VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total VWF
[PROOF STEP]
using VWF_def total_VWOId
[PROOF STATE]
proof (prove)
using this:
VWF \<equiv> VWO - Id
total (VWO - Id)

goal (1 subgoal):
 1. total VWF
[PROOF STEP]
by auto


[STATEMENT]
lemma total_on_VWF [iff]: "total_on A VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_on A VWF
[PROOF STEP]
by (meson UNIV_I total_VWF total_on_def)


[STATEMENT]
lemma VWF_asym:
  assumes "(x,y) \<in> VWF" "(y,x) \<in> VWF" shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using VWF_def assms wf_VWO wf_not_sym
[PROOF STATE]
proof (prove)
using this:
VWF \<equiv> VWO - Id
(x, y) \<in> VWF
(y, x) \<in> VWF
wf (VWO - Id)
\<lbrakk>wf ?r; (?a, ?x) \<in> ?r\<rbrakk> \<Longrightarrow> (?x, ?a) \<notin> ?r

goal (1 subgoal):
 1. False
[PROOF STEP]
by fastforce


[STATEMENT]
lemma VWF_non_refl [iff]: "(x,x) \<notin> VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, x) \<notin> VWF
[PROOF STEP]
by simp


[STATEMENT]
lemma VWF_iff_Ord_less [simp]: "\<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> (\<alpha>,\<beta>) \<in> VWF \<longleftrightarrow> \<alpha> < \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, \<beta>) \<in> VWF) = (\<alpha> < \<beta>)
[PROOF STEP]
by (simp add: VWF_def less_V_def)


[STATEMENT]
lemma mem_imp_VWF: "x \<in> elts y \<Longrightarrow> (x,y) \<in> VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> elts y \<Longrightarrow> (x, y) \<in> VWF
[PROOF STEP]
using VWF_def mem_imp_VWO
[PROOF STATE]
proof (prove)
using this:
VWF \<equiv> VWO - Id
?x \<in> elts ?y \<Longrightarrow> (?x, ?y) \<in> VWO

goal (1 subgoal):
 1. x \<in> elts y \<Longrightarrow> (x, y) \<in> VWF
[PROOF STEP]
by fastforce


[STATEMENT]
lemma ordermap_type:
    "small A \<Longrightarrow> ordermap A r \<in> A \<rightarrow> elts (ordertype A r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small A \<Longrightarrow> ordermap A r \<in> A \<rightarrow> elts (ordertype A r)
[PROOF STEP]
by (simp add: ordertype_def)


[STATEMENT]
lemma ordermap_in_ordertype [intro]: "\<lbrakk>a \<in> A; small A\<rbrakk> \<Longrightarrow> ordermap A r a \<in> elts (ordertype A r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> A; small A\<rbrakk> \<Longrightarrow> ordermap A r a \<in> elts (ordertype A r)
[PROOF STEP]
by (simp add: ordertype_def)


[STATEMENT]
lemma ordermap: "wf r \<Longrightarrow> ordermap A r a = set (ordermap A r ` {y \<in> A. (y,a) \<in> r})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf r \<Longrightarrow> ordermap A r a = set (ordermap A r ` {y \<in> A. (y, a) \<in> r})
[PROOF STEP]
unfolding ordermap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf r \<Longrightarrow> wfrec r (\<lambda>f x. set (f ` {y \<in> A. (y, x) \<in> r})) a = set (wfrec r (\<lambda>f x. set (f ` {y \<in> A. (y, x) \<in> r})) ` {y \<in> A. (y, a) \<in> r})
[PROOF STEP]
by (auto simp: wfrec_fixpoint adm_wf_def)