[STATEMENT]
lemma (in pcategory) pcat_vsubset_index_pcategory:
  assumes "J \<subseteq>\<^sub>\<circ> I"
  shows "pcategory \<alpha> J \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcategory \<alpha> J \<AA>
[PROOF STEP]
proof(intro pcategoryI pcategory_psemicategoryI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pcategory_base \<alpha> J \<AA>
 2. \<And>Ja. Ja \<subseteq>\<^sub>\<circ> J \<Longrightarrow> cat_prod Ja \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 3. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>" if \<open>J' \<subseteq>\<^sub>\<circ> J\<close> for J'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from that assms
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
have "J' \<subseteq>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I

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

goal (1 subgoal):
 1. cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
show "cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule pcat_Obj_vsubset_Vset)
[PROOF STATE]
proof (state)
this:
cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?J' \<subseteq>\<^sub>\<circ> J \<Longrightarrow> cat_prod ?J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. pcategory_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
fix A B J'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pcategory_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
assume prems:
    "J' \<subseteq>\<^sub>\<circ> J"
    "A \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>Ci\<in>\<^sub>\<circ>J'. \<AA> i)\<lparr>Obj\<rparr>"
    "B \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>Ci\<in>\<^sub>\<circ>J'. \<AA> i)\<lparr>Obj\<rparr>"
    "A \<in>\<^sub>\<circ> Vset \<alpha>" 
    "B \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (state)
this:
J' \<subseteq>\<^sub>\<circ> J
A \<subseteq>\<^sub>\<circ> cat_prod J' \<AA>\<lparr>Obj\<rparr>
B \<subseteq>\<^sub>\<circ> cat_prod J' \<AA>\<lparr>Obj\<rparr>
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. pcategory_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "(\<Union>\<^sub>\<circ>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>B. Hom (\<Prod>\<^sub>Ci\<in>\<^sub>\<circ>J'. \<AA> i) a b) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from prems(1) assms
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
have "J' \<subseteq>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I

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

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from pcat_Hom_vifunion_in_Vset[OF this prems(2-5)]
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. pcategory_base \<alpha> J \<AA>
[PROOF STEP]
qed (rule pcat_vsubset_index_pcategory_base[OF assms])