[STATEMENT]
lemma (in category) cat_cf_parallel_\<bb>\<aa>:
  assumes "vsv F'"
    and "F \<in>\<^sub>\<circ> Vset \<alpha>" 
    and "\<D>\<^sub>\<circ> F' = F"
    and "\<And>\<ff>. \<ff> \<in>\<^sub>\<circ> F \<Longrightarrow> F'\<lparr>\<ff>\<rparr> : \<bb> \<mapsto>\<^bsub>\<CC>\<^esub> \<aa>"
    and "\<aa> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
    and "\<bb> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
  shows "cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>
[PROOF STEP]
have "\<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>" "\<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha> &&& \<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp_all add: Axiom_of_Pairing \<bb>\<^sub>P\<^sub>L_def \<aa>\<^sub>P\<^sub>L_def assms(2))
[PROOF STATE]
proof (state)
this:
\<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
\<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
\<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
\<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>
[PROOF STEP]
by (intro cf_parallelI cat_parallelI)
      (simp_all add: assms cat_parallel_cs_intros cat_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>

goal:
No subgoals!
[PROOF STEP]
qed