[STATEMENT]
lemma part_UN:
assumes "\<And> n. n \<in> N \<Longrightarrow> part (I n) (P n)"
and "\<And> n1 n2. {n1,n2} \<subseteq> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}"
shows "part (UN n : N. I n) (UN n : N. P n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part (\<Union> (I ` N)) (\<Union> (P ` N))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?n \<in> N \<Longrightarrow> part (I ?n) (P ?n)
{?n1.0, ?n2.0} \<subseteq> N \<and> ?n1.0 \<noteq> ?n2.0 \<Longrightarrow> I ?n1.0 \<inter> I ?n2.0 = {}

goal (1 subgoal):
 1. part (\<Union> (I ` N)) (\<Union> (P ` N))
[PROOF STEP]
unfolding part_def
[PROOF STATE]
proof (prove)
using this:
?n \<in> N \<Longrightarrow> \<Union> (P ?n) = I ?n \<and> (\<forall>J1 J2. J1 \<in> P ?n \<and> J2 \<in> P ?n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {})
{?n1.0, ?n2.0} \<subseteq> N \<and> ?n1.0 \<noteq> ?n2.0 \<Longrightarrow> I ?n1.0 \<inter> I ?n2.0 = {}

goal (1 subgoal):
 1. \<Union> (\<Union> (P ` N)) = \<Union> (I ` N) \<and> (\<forall>J1 J2. J1 \<in> \<Union> (P ` N) \<and> J2 \<in> \<Union> (P ` N) \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; xa \<in> N; x \<in> I xa\<rbrakk> \<Longrightarrow> \<exists>y\<in>N. \<exists>xa\<in>P y. x \<in> xa
 2. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J1; xb \<notin> J2; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
 3. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J2; xb \<notin> J1; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis UnionE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J1; xb \<notin> J2; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
 2. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J2; xb \<notin> J1; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Union_upper disjoint_iff_not_equal insert_absorb insert_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J2; xb \<notin> J1; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis UnionI disjoint_iff_not_equal)