[STATEMENT]
lemma finite_subset_chain:
  fixes Y :: "nat \<Rightarrow> 'a set"
  assumes "chain Y"
  assumes "S \<subseteq> \<Union>(Y ` UNIV)"
  assumes "finite S"
  shows "\<exists>i. S \<subseteq> Y i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> \<Union> (range Y)
[PROOF STEP]
have "\<forall>x \<in> S. \<exists> i. x \<in> Y i"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> \<Union> (range Y)

goal (1 subgoal):
 1. \<forall>x\<in>S. \<exists>i. x \<in> Y i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. \<exists>i. x \<in> Y i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. \<exists>i. x \<in> Y i
[PROOF STEP]
obtain f where f: "\<forall> x\<in> S. x \<in> Y (f x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. \<exists>i. x \<in> Y i

goal (1 subgoal):
 1. (\<And>f. \<forall>x\<in>S. x \<in> Y (f x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. x \<in> Y (f x)

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
define i where "i = Max (f ` S)"
[PROOF STATE]
proof (state)
this:
i = Max (f ` S)

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
from \<open>finite S\<close>
[PROOF STATE]
proof (chain)
picking this:
finite S
[PROOF STEP]
have "finite (f ` S)"
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. finite (f ` S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (f ` S)

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
hence "\<forall> x\<in>S. f x \<le> i"
[PROOF STATE]
proof (prove)
using this:
finite (f ` S)

goal (1 subgoal):
 1. \<forall>x\<in>S. f x \<le> i
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
using this:
finite (f ` S)

goal (1 subgoal):
 1. \<forall>x\<in>S. f x \<le> Max (f ` S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. f x \<le> i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
with chain_mono[OF \<open>chain Y\<close>]
[PROOF STATE]
proof (chain)
picking this:
?i \<le> ?j \<Longrightarrow> Y ?i \<sqsubseteq> Y ?j
\<forall>x\<in>S. f x \<le> i
[PROOF STEP]
have "\<forall> x\<in>S. Y (f x) \<subseteq> Y i"
[PROOF STATE]
proof (prove)
using this:
?i \<le> ?j \<Longrightarrow> Y ?i \<sqsubseteq> Y ?j
\<forall>x\<in>S. f x \<le> i

goal (1 subgoal):
 1. \<forall>x\<in>S. Y (f x) \<subseteq> Y i
[PROOF STEP]
by (auto simp add: below_set_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. Y (f x) \<subseteq> Y i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. x \<in> Y (f x)
\<forall>x\<in>S. Y (f x) \<subseteq> Y i
[PROOF STEP]
have "S \<subseteq> Y i"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. x \<in> Y (f x)
\<forall>x\<in>S. Y (f x) \<subseteq> Y i

goal (1 subgoal):
 1. S \<subseteq> Y i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<subseteq> Y i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> Y i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>i. S \<subseteq> Y i

goal:
No subgoals!
[PROOF STEP]
qed