[STATEMENT]
lemma (in pdigraph) pdg_dghm_up_eq_dghm_proj:
  assumes "\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
    and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i = \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>"
  shows "dghm_up I \<AA> \<CC> \<phi> = \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi> = \<FF>
[PROOF STEP]
proof(rule dghm_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. dghm_up I \<AA> \<CC> \<phi> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<FF> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\

 3. dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
 4. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
interpret \<FF>: is_dghm \<alpha> \<CC> \<open>(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<close> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. dghm_up I \<AA> \<CC> \<phi> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<FF> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\

 3. dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
 4. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
show "dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
[PROOF STEP]
proof(rule pdg_dghm_up_is_dghm)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. digraph \<alpha> \<CC>
 2. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. digraph \<alpha> \<CC>
 2. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
assume prems: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (2 subgoals):
 1. digraph \<alpha> \<CC>
 2. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
interpret \<pi>: is_dghm \<alpha> \<open>(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<close> \<open>\<AA> i\<close> \<open>\<pi>\<^sub>D\<^sub>G I \<AA> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule pdg_dghm_proj_is_dghm)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. digraph \<alpha> \<CC>
 2. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
show "\<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
unfolding assms(2)[OF prems]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i

goal (1 subgoal):
 1. digraph \<alpha> \<CC>
[PROOF STEP]
qed (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>

goal (5 subgoals):
 1. \<FF> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\

 2. dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
 3. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 4. \<CC> = ?\<CC>
 5. dg_prod I \<AA> = ?\

[PROOF STEP]
show "dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dghm_up_ObjMap_vdomain)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 3. \<CC>\<lparr>Obj\<rparr> = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 3. \<CC>\<lparr>Obj\<rparr> = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 3. \<CC>\<lparr>Obj\<rparr> = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dghm_up_ObjMap_app_vdomain[OF prems])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 3. I = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. \<And>aa. aa \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 3. I = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. \<And>aa. aa \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
assume prems': "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 3. I = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. \<And>aa. aa \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
with pdg_dghm_proj_is_dghm[OF prems'] \<FF>.is_dghm_axioms prems
[PROOF STATE]
proof (chain)
picking this:
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show
        "dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: dg_cs_simps assms(2) cs_intro: dg_cs_intros
          )
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>

goal (3 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 3. I = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
qed
      (
        use \<FF>.dghm_ObjMap_app_in_HomCod_Obj prems in
          \<open>auto simp: dg_prod_components dghm_up_ObjMap_app\<close>
      )
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 3. \<CC>\<lparr>Obj\<rparr> = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
qed (auto simp: dghm_up_components dg_cs_simps)
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>

goal (4 subgoals):
 1. \<FF> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\

 2. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 3. \<CC> = ?\<CC>
 4. dg_prod I \<AA> = ?\

[PROOF STEP]
show "dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dghm_up_ArrMap_vdomain)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<CC>\<lparr>Arr\<rparr> = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<CC>\<lparr>Arr\<rparr> = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<CC>\<lparr>Arr\<rparr> = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dghm_up_ArrMap_app_vdomain[OF prems])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 3. I = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 4. \<And>aa. aa \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 3. I = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 4. \<And>aa. aa \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
assume prems': "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (4 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 3. I = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 4. \<And>aa. aa \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
with pdg_dghm_proj_is_dghm[OF prems'] \<FF>.is_dghm_axioms prems
[PROOF STATE]
proof (chain)
picking this:
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show
        "dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: dg_cs_simps assms(2) cs_intro: dg_cs_intros
          )
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>

goal (3 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 3. I = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
qed
      (
        use \<FF>.dghm_ArrMap_app_in_HomCod_Arr prems in
          \<open>auto simp: dg_prod_components dghm_up_ArrMap_app\<close>
      )+
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<CC>\<lparr>Arr\<rparr> = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
qed (auto simp: dghm_up_components dg_cs_simps)
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>

goal (3 subgoals):
 1. \<FF> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\

 2. \<CC> = ?\<CC>
 3. dg_prod I \<AA> = ?\

[PROOF STEP]
qed (simp_all add: assms(1))


[STATEMENT]
lemma dg_singleton_ObjI:
  assumes "A = set {\<langle>j, a\<rangle>}" and "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
  shows "A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<lparr>Obj\<rparr>)
[PROOF STEP]
by auto


[STATEMENT]
lemma dg_singleton_ObjE:
  assumes "A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Obj\<rparr>"
  obtains a where "A = set {\<langle>j, a\<rangle>}" and "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vproductD[OF assms[unfolded dg_prod_components], rule_format]
[PROOF STATE]
proof (chain)
picking this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
have "vsv A" and [simp]: "\<D>\<^sub>\<circ> A = set {j}" and Aj: "A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv A &&& \<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j} &&& A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
interpret A: vsv A
[PROOF STATE]
proof (prove)
using this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from A.vsv_is_VLambda
[PROOF STATE]
proof (chain)
picking this:
VLambda (\<D>\<^sub>\<circ> A) (app A) = A
[PROOF STEP]
have "A = set {\<langle>j, A\<lparr>j\<rparr>\<rangle>}"
[PROOF STATE]
proof (prove)
using this:
VLambda (\<D>\<^sub>\<circ> A) (app A) = A

goal (1 subgoal):
 1. A = ZFC_in_HOL.set {\<langle>j, A\<lparr>j\<rparr>\<rangle>}
[PROOF STEP]
by (auto simp: VLambda_vsingleton)
[PROOF STATE]
proof (state)
this:
A = ZFC_in_HOL.set {\<langle>j, A\<lparr>j\<rparr>\<rangle>}

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with Aj
[PROOF STATE]
proof (chain)
picking this:
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
A = ZFC_in_HOL.set {\<langle>j, A\<lparr>j\<rparr>\<rangle>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
A = ZFC_in_HOL.set {\<langle>j, A\<lparr>j\<rparr>\<rangle>}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
A = ZFC_in_HOL.set {\<langle>j, A\<lparr>j\<rparr>\<rangle>}
\<lbrakk>A = ZFC_in_HOL.set {\<langle>j, ?a\<rangle>}; ?a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_singleton_ArrI:
  assumes "F = set {\<langle>j, a\<rangle>}" and "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
  shows "F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
F = ZFC_in_HOL.set {\<langle>j, a\<rangle>}
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
F = ZFC_in_HOL.set {\<langle>j, a\<rangle>}
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. F \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<lparr>Arr\<rparr>)
[PROOF STEP]
by auto


[STATEMENT]
lemma dg_singleton_ArrE:
  assumes "F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Arr\<rparr>"
  obtains a where "F = set {\<langle>j, a\<rangle>}" and "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>F = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>F = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vproductD[OF assms[unfolded dg_prod_components], rule_format]
[PROOF STATE]
proof (chain)
picking this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
have "vsv F" and [simp]: "\<D>\<^sub>\<circ> F = set {j}" and Fj: "F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv F &&& \<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j} &&& F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>F = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret F: vsv F
[PROOF STATE]
proof (prove)
using this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>F = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from F.vsv_is_VLambda
[PROOF STATE]
proof (chain)
picking this:
VLambda (\<D>\<^sub>\<circ> F) (app F) = F
[PROOF STEP]
have "F = set {\<langle>j, F\<lparr>j\<rparr>\<rangle>}"
[PROOF STATE]
proof (prove)
using this:
VLambda (\<D>\<^sub>\<circ> F) (app F) = F

goal (1 subgoal):
 1. F = ZFC_in_HOL.set {\<langle>j, F\<lparr>j\<rparr>\<rangle>}
[PROOF STEP]
by (auto simp: VLambda_vsingleton)
[PROOF STATE]
proof (state)
this:
F = ZFC_in_HOL.set {\<langle>j, F\<lparr>j\<rparr>\<rangle>}

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>F = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with Fj
[PROOF STATE]
proof (chain)
picking this:
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
F = ZFC_in_HOL.set {\<langle>j, F\<lparr>j\<rparr>\<rangle>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
F = ZFC_in_HOL.set {\<langle>j, F\<lparr>j\<rparr>\<rangle>}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
F = ZFC_in_HOL.set {\<langle>j, F\<lparr>j\<rparr>\<rangle>}
\<lbrakk>F = ZFC_in_HOL.set {\<langle>j, ?a\<rangle>}; ?a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in digraph) dg_finite_pdigraph_dg_singleton:
  assumes "j \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "finite_pdigraph \<alpha> (set {j}) (\<lambda>i. \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha> (ZFC_in_HOL.set {j}) (\<lambda>i. \<CC>)
[PROOF STEP]
by (intro finite_pdigraphI pdigraph_baseI)
    (auto simp: digraph_axioms Limit_vsingleton_in_VsetI assms)


[STATEMENT]
lemma (in digraph) dg_digraph_dg_singleton:
  assumes "j \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
interpret finite_pdigraph \<alpha> \<open>set {j}\<close> \<open>\<lambda>i. \<CC>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha> (ZFC_in_HOL.set {j}) (\<lambda>i. \<CC>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. finite_pdigraph \<alpha> (ZFC_in_HOL.set {j}) (\<lambda>i. \<CC>)
[PROOF STEP]
by (rule dg_finite_pdigraph_dg_singleton)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
by (rule pdg_digraph_dg_prod)
[PROOF STATE]
proof (state)
this:
digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in digraph) dg_singleton_is_arrI:
  assumes "j \<in>\<^sub>\<circ> Vset \<alpha>" and "f : a \<mapsto>\<^bsub>\<CC>\<^esub> b"
  shows "set {\<langle>j, f\<rangle>} : set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>(\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<^esub> set {\<langle>j, b\<rangle>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set {\<langle>j, f\<rangle>} : ZFC_in_HOL.set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> ZFC_in_HOL.set {\<langle>j, b\<rangle>}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ZFC_in_HOL.set {\<langle>j, f\<rangle>} : ZFC_in_HOL.set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> ZFC_in_HOL.set {\<langle>j, b\<rangle>}
[PROOF STEP]
interpret finite_pdigraph \<alpha> \<open>set {j}\<close> \<open>\<lambda>i. \<CC>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha> (ZFC_in_HOL.set {j}) (\<lambda>i. \<CC>)
[PROOF STEP]
by (rule dg_finite_pdigraph_dg_singleton[OF assms(1)])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ZFC_in_HOL.set {\<langle>j, f\<rangle>} : ZFC_in_HOL.set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> ZFC_in_HOL.set {\<langle>j, b\<rangle>}
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b

goal (1 subgoal):
 1. ZFC_in_HOL.set {\<langle>j, f\<rangle>} : ZFC_in_HOL.set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> ZFC_in_HOL.set {\<langle>j, b\<rangle>}
[PROOF STEP]
by (intro dg_prod_is_arrI) auto
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set {\<langle>j, f\<rangle>} : ZFC_in_HOL.set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> ZFC_in_HOL.set {\<langle>j, b\<rangle>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in digraph) dg_singleton_is_arrD:
  assumes "set {\<langle>j, f\<rangle>} : set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>(\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<^esub> set {\<langle>j, b\<rangle>}"
    and "j \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "f : a \<mapsto>\<^bsub>\<CC>\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
interpret finite_pdigraph \<alpha> \<open>set {j}\<close> \<open>\<lambda>i. \<CC>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha> (ZFC_in_HOL.set {j}) (\<lambda>i. \<CC>)
[PROOF STEP]
by (rule dg_finite_pdigraph_dg_singleton[OF assms(2)])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
from dg_prod_is_arrD(7)[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> ZFC_in_HOL.set {\<langle>j, f\<rangle>}\<lparr>?i\<rparr> : ZFC_in_HOL.set {\<langle>j, a\<rangle>}\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> ZFC_in_HOL.set {\<langle>j, b\<rangle>}\<lparr>?i\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> ZFC_in_HOL.set {\<langle>j, f\<rangle>}\<lparr>?i\<rparr> : ZFC_in_HOL.set {\<langle>j, a\<rangle>}\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> ZFC_in_HOL.set {\<langle>j, b\<rangle>}\<lparr>?i\<rparr>

goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in digraph) dg_singleton_is_arrE:
  assumes "set {\<langle>j, f\<rangle>} : set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>(\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<^esub> set {\<langle>j, b\<rangle>}"
    and "j \<in>\<^sub>\<circ> Vset \<alpha>"
  obtains "f : a \<mapsto>\<^bsub>\<CC>\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms dg_singleton_is_arrD
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.set {\<langle>j, f\<rangle>} : ZFC_in_HOL.set {\<langle>j, a\<rangle>} \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> ZFC_in_HOL.set {\<langle>j, b\<rangle>}
j \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>ZFC_in_HOL.set {\<langle>?j, ?f\<rangle>} : ZFC_in_HOL.set {\<langle>?j, ?a\<rangle>} \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {?j}. \<CC>\<^esub> ZFC_in_HOL.set {\<langle>?j, ?b\<rangle>}; ?j \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> ?f : ?a \<mapsto>\<^bsub>\<CC>\<^esub> ?b

goal (1 subgoal):
 1. (f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma dghm_singleton_components:
  shows "dghm_singleton j \<CC>\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. set {\<langle>j, a\<rangle>})"
    and "dghm_singleton j \<CC>\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. set {\<langle>j, f\<rangle>})"
    and "dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC>"
    and "dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>}) &&& dghm_singleton j \<CC>\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})) &&& dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC> &&& dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
unfolding dghm_singleton_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>}, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>}, \<CC>, \<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>}) &&& [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>}, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>}, \<CC>, \<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})) &&& [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>}, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>}, \<CC>, \<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<CC> &&& [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>}, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>}, \<CC>, \<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma dghm_singleton_ObjMap_vrange[dg_cs_simps]:
  "\<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
assume "A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
obtain a where A_def: "A = set {\<langle>j, a\<rangle>}" and a: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dghm_singleton_components
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>})

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}; a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
show "A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
A = ZFC_in_HOL.set {\<langle>j, a\<rangle>}
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<lparr>Obj\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
assume "A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
from vproductD[OF this[unfolded dg_prod_components], rule_format]
[PROOF STATE]
proof (chain)
picking this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
have "vsv A"
    and [simp]: "\<D>\<^sub>\<circ> A = set {j}"
    and Ai: "\<And>i. i \<in>\<^sub>\<circ> set {j} \<Longrightarrow> A\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv A &&& \<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j} &&& (\<And>i. i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
interpret A: vsv A
[PROOF STATE]
proof (prove)
using this:
vsv A
\<D>\<^sub>\<circ> A = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
from Ai
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
have "A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
using Ai
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> A\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
with A.vsv_is_VLambda
[PROOF STATE]
proof (chain)
picking this:
VLambda (\<D>\<^sub>\<circ> A) (app A) = A
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
have "A = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. set {\<langle>j, f\<rangle>})\<lparr>A\<lparr>j\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
VLambda (\<D>\<^sub>\<circ> A) (app A) = A
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. A = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>A\<lparr>j\<rparr>\<rparr>
[PROOF STEP]
by (simp add: VLambda_vsingleton)
[PROOF STATE]
proof (state)
this:
A = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>A\<lparr>j\<rparr>\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
A = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>A\<lparr>j\<rparr>\<rparr>
[PROOF STEP]
show "A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
A = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>A\<lparr>j\<rparr>\<rparr>

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
unfolding dghm_singleton_components
[PROOF STATE]
proof (prove)
using this:
A\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
A = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>A\<lparr>j\<rparr>\<rparr>

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>})
[PROOF STEP]
by
      (
        metis
          dghm_singleton_ObjMap_vdomain
          dghm_singleton_ObjMap_vsv
          dghm_singleton_components(1)
          vsv.vsv_vimageI2
      )
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_singleton_ArrMap_vrange[dg_cs_simps]:
  "\<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
assume "F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (state)
this:
F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
obtain f where "F = set {\<langle>j, f\<rangle>}" and "f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>F = ZFC_in_HOL.set {\<langle>j, f\<rangle>}; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dghm_singleton_components
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>F = ZFC_in_HOL.set {\<langle>j, f\<rangle>}; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F = ZFC_in_HOL.set {\<langle>j, f\<rangle>}
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F = ZFC_in_HOL.set {\<langle>j, f\<rangle>}
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show "F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
F = ZFC_in_HOL.set {\<langle>j, f\<rangle>}
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
F = ZFC_in_HOL.set {\<langle>j, f\<rangle>}
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. F \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<lparr>Arr\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
assume "F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
F \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
from vproductD[OF this[unfolded dg_prod_components], rule_format]
[PROOF STATE]
proof (chain)
picking this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
have "vsv F"
    and [simp]: "\<D>\<^sub>\<circ> F = set {j}"
    and Fi: "\<And>i. i \<in>\<^sub>\<circ> set {j} \<Longrightarrow> F\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv F &&& \<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j} &&& (\<And>i. i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret F: vsv F
[PROOF STATE]
proof (prove)
using this:
vsv F
\<D>\<^sub>\<circ> F = ZFC_in_HOL.set {j}
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
from Fi
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
have "F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
using Fi
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
?i \<in>\<^sub>\<circ> ZFC_in_HOL.set {j} \<Longrightarrow> F\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
with F.vsv_is_VLambda
[PROOF STATE]
proof (chain)
picking this:
VLambda (\<D>\<^sub>\<circ> F) (app F) = F
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
have "F = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. set {\<langle>j, f\<rangle>})\<lparr>F\<lparr>j\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
VLambda (\<D>\<^sub>\<circ> F) (app F) = F
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. F = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>F\<lparr>j\<rparr>\<rparr>
[PROOF STEP]
by (simp add: VLambda_vsingleton)
[PROOF STATE]
proof (state)
this:
F = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>F\<lparr>j\<rparr>\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
F = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>F\<lparr>j\<rparr>\<rparr>
[PROOF STEP]
show "F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
F = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>F\<lparr>j\<rparr>\<rparr>

goal (1 subgoal):
 1. F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
unfolding dghm_singleton_components
[PROOF STATE]
proof (prove)
using this:
F\<lparr>j\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
F = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})\<lparr>F\<lparr>j\<rparr>\<rparr>

goal (1 subgoal):
 1. F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>})
[PROOF STEP]
by
      (
        metis
          dghm_singleton_ArrMap_vdomain
          dghm_singleton_ArrMap_vsv
          dghm_singleton_components(2)
          vsv.vsv_vimageI2
      )
[PROOF STATE]
proof (state)
this:
F \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in digraph) dg_dghm_singleton_is_dghm:
  assumes "j \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "dghm_singleton j \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_singleton j \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dghm_singleton j \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
interpret finite_pdigraph \<alpha> \<open>set {j}\<close> \<open>\<lambda>i. \<CC>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha> (ZFC_in_HOL.set {j}) (\<lambda>i. \<CC>)
[PROOF STEP]
by (rule dg_finite_pdigraph_dg_singleton[OF assms])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dghm_singleton j \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_singleton j \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
[PROOF STEP]
proof(intro is_iso_dghmI is_dghmI)
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (dghm_singleton j \<CC>)
 3. digraph \<alpha> \<CC>
 4. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 5. vcard (dghm_singleton j \<CC>) = 4\<^sub>\<nat>
 6. dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC>
 7. dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 8. vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
 9. vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
A total of 17 subgoals...
[PROOF STEP]
show "vfsequence (dghm_singleton j \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (dghm_singleton j \<CC>)
[PROOF STEP]
unfolding dghm_singleton_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>}, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>}, \<CC>, \<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (dghm_singleton j \<CC>)

goal (16 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 4. vcard (dghm_singleton j \<CC>) = 4\<^sub>\<nat>
 5. dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC>
 6. dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 7. vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
 8. vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
 9. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 10. \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
A total of 16 subgoals...
[PROOF STEP]
show "vcard (dghm_singleton j \<CC>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (dghm_singleton j \<CC>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dghm_singleton_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. ZFC_in_HOL.set {\<langle>j, a\<rangle>}, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. ZFC_in_HOL.set {\<langle>j, f\<rangle>}, \<CC>, \<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (dghm_singleton j \<CC>) = 4\<^sub>\<nat>

goal (15 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 4. dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC>
 5. dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 6. vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
A total of 15 subgoals...
[PROOF STEP]
show "\<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>

goal (14 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 4. dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC>
 5. dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 6. vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
A total of 14 subgoals...
[PROOF STEP]
show "dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> :
      dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>\<^esub>
      dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
      if "f : a \<mapsto>\<^bsub>\<CC>\<^esub> b" for f a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b

goal (1 subgoal):
 1. dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
proof(intro dg_prod_is_arrI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = ZFC_in_HOL.set {j}
 3. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = ZFC_in_HOL.set {j}
 5. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = ZFC_in_HOL.set {j}
 7. \<And>ja. \<lbrakk>f : a \<mapsto>\<^bsub>\<CC>\<^esub> b; ja \<in>\<^sub>\<circ> ZFC_in_HOL.set {j}\<rbrakk> \<Longrightarrow> dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>ja\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>ja\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>ja\<rparr>
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = ZFC_in_HOL.set {j}
 3. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = ZFC_in_HOL.set {j}
 5. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = ZFC_in_HOL.set {j}
 7. \<And>ja. \<lbrakk>f : a \<mapsto>\<^bsub>\<CC>\<^esub> b; ja \<in>\<^sub>\<circ> ZFC_in_HOL.set {j}\<rbrakk> \<Longrightarrow> dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>ja\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>ja\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>ja\<rparr>
[PROOF STEP]
assume "k \<in>\<^sub>\<circ> set {j}"
[PROOF STATE]
proof (state)
this:
k \<in>\<^sub>\<circ> ZFC_in_HOL.set {j}

goal (7 subgoals):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = ZFC_in_HOL.set {j}
 3. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = ZFC_in_HOL.set {j}
 5. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = ZFC_in_HOL.set {j}
 7. \<And>ja. \<lbrakk>f : a \<mapsto>\<^bsub>\<CC>\<^esub> b; ja \<in>\<^sub>\<circ> ZFC_in_HOL.set {j}\<rbrakk> \<Longrightarrow> dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>ja\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>ja\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>ja\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in>\<^sub>\<circ> ZFC_in_HOL.set {j}
[PROOF STEP]
have k_def: "k = j"
[PROOF STATE]
proof (prove)
using this:
k \<in>\<^sub>\<circ> ZFC_in_HOL.set {j}

goal (1 subgoal):
 1. k = j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k = j

goal (7 subgoals):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = ZFC_in_HOL.set {j}
 3. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = ZFC_in_HOL.set {j}
 5. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = ZFC_in_HOL.set {j}
 7. \<And>ja. \<lbrakk>f : a \<mapsto>\<^bsub>\<CC>\<^esub> b; ja \<in>\<^sub>\<circ> ZFC_in_HOL.set {j}\<rbrakk> \<Longrightarrow> dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>ja\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>ja\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>ja\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
show "dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>k\<rparr> :
        dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>k\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>k\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b

goal (1 subgoal):
 1. dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>k\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>k\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>k\<rparr>
[PROOF STEP]
by
          (
            cs_concl
              cs_simp: k_def V_cs_simps dg_cs_simps dg_prod_cs_simps
              cs_intro: dg_cs_intros
          )
[PROOF STATE]
proof (state)
this:
dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>k\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>k\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>k\<rparr>

goal (6 subgoals):
 1. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = ZFC_in_HOL.set {j}
 3. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = ZFC_in_HOL.set {j}
 5. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = ZFC_in_HOL.set {j}
[PROOF STEP]
qed
      (
        cs_concl
          cs_simp: V_cs_simps dg_prod_cs_simps
          cs_intro: V_cs_intros dg_cs_intros
      )+
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>\<CC>\<^esub> ?b \<Longrightarrow> dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> : dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>\<^esub> dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>\<lparr>?b\<rparr>

goal (13 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 4. dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC>
 5. dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 6. vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
 10. v11 (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
A total of 13 subgoals...
[PROOF STEP]
show "\<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Obj\<rparr>

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 4. dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC>
 5. dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 6. vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
 10. v11 (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
A total of 12 subgoals...
[PROOF STEP]
show "\<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>set {j}. \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)\<lparr>Arr\<rparr>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 4. dghm_singleton j \<CC>\<lparr>HomDom\<rparr> = \<CC>
 5. dghm_singleton j \<CC>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)
 6. vsv (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_singleton j \<CC>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
 10. v11 (dghm_singleton j \<CC>\<lparr>ObjMap\<rparr>)
A total of 11 subgoals...
[PROOF STEP]
qed
    (
      auto simp:
        dg_cs_intros
        dg_digraph_dg_singleton[OF assms]
        dghm_singleton_components
    )
[PROOF STATE]
proof (state)
this:
dghm_singleton j \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>ZFC_in_HOL.set {j}. \<CC>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_pdigraph_dg_prod_2: "finite_pdigraph \<alpha> (2\<^sub>\<nat>) (if2 \<AA> \<BB>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha> (2\<^sub>\<nat>) (\<lambda>i. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)
[PROOF STEP]
proof(intro finite_pdigraphI pdigraph_baseI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<Z> \<alpha>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> digraph \<alpha> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)
 3. 2\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
 4. vfinite (2\<^sub>\<nat>)
[PROOF STEP]
from Axiom_of_Infinity
[PROOF STATE]
proof (chain)
picking this:
\<omega> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show z1_in_Vset: "2\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<omega> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. 2\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
2\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>

goal (3 subgoals):
 1. \<Z> \<alpha>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> digraph \<alpha> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)
 3. vfinite (2\<^sub>\<nat>)
[PROOF STEP]
show "digraph \<alpha> (i = 0 ? \<AA> : \<BB>)" if "i \<in>\<^sub>\<circ> 2\<^sub>\<nat>" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)
[PROOF STEP]
by (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> digraph \<alpha> (if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)

goal (2 subgoals):
 1. \<Z> \<alpha>
 2. vfinite (2\<^sub>\<nat>)
[PROOF STEP]
qed auto


[STATEMENT]
lemma digraph_dg_prod_2[dg_cs_intros]: "digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)
[PROOF STEP]
unfolding dg_prod_2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>2\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)
[PROOF STEP]
by (rule pdg_digraph_dg_prod)
[PROOF STATE]
proof (state)
this:
digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_ObjI:
  assumes "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
  shows "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)
[PROOF STEP]
proof(intro vproductI ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv [a, b]\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>
 3. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps two)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>

goal (2 subgoals):
 1. vsv [a, b]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv [a, b]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> 2\<^sub>\<nat>"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>

goal (2 subgoals):
 1. vsv [a, b]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>
[PROOF STEP]
consider \<open>i = 0\<close> | \<open>i = 1\<^sub>\<nat>\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding two
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> ZFC_in_HOL.set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. vsv [a, b]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "[a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = 0 then \<AA> else \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by cases (simp_all add: nat_omega_simps assms(1,2))
[PROOF STATE]
proof (state)
this:
[a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv [a, b]\<^sub>\<circ>
[PROOF STEP]
qed auto


[STATEMENT]
lemma dg_prod_2_ObjI'[dg_prod_cs_intros]:
  assumes "ab = [a, b]\<^sub>\<circ>" and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
  shows "ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding assms(1)
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (rule dg_prod_2_ObjI)


[STATEMENT]
lemma dg_prod_2_ObjE:
  assumes "ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
  obtains a b where "ab = [a, b]\<^sub>\<circ>" and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vproductD[OF assms[unfolded dg_prod_2_def dg_prod_components]]
[PROOF STATE]
proof (chain)
picking this:
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
\<forall>i\<in>elts (2\<^sub>\<nat>). ab\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
have vsv_ab: "vsv ab"
    and dom_ab: "\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>"
    and ab_app: "\<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> ab\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = 0 then \<AA> else \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
\<forall>i\<in>elts (2\<^sub>\<nat>). ab\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv ab &&& \<D>\<^sub>\<circ> ab = 2\<^sub>\<nat> &&& (\<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> ab\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> ab\<lparr>?i\<rparr> \<in>\<^sub>\<circ> (if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have dom_ab[simp]: "\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
[PROOF STEP]
unfolding dom_ab
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2\<^sub>\<nat> = 2\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps two)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret vsv ab
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ab
[PROOF STEP]
by (rule vsv_ab)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "ab = [vpfst ab, vpsnd ab]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (rule vsv_vfsequence_two[symmetric]) auto
[PROOF STATE]
proof (state)
this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from ab_app[of 0]
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> ab\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
have "vpfst ab \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> ab\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ab\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ab\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from ab_app[of \<open>1\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> ab\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
have "vpsnd ab \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> ab\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ab\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ab\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
ab\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
ab\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
ab\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
\<lbrakk>ab = [?a, ?b]\<^sub>\<circ>; ?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed