[STATEMENT]
lemma bij_betw_hom_vfun:
    shows "V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b))"
    and "\<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b"
    and "f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f"
    and "\<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk>
            \<Longrightarrow> V_of_arr (arr_of_V a b F) = F"
    and "\<lbrakk>ide a; ide b\<rbrakk>
            \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))"
    and "\<lbrakk>ide a; ide b\<rbrakk>
            \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)) &&& (\<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b) &&& (f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f)) &&& (\<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F) &&& (\<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))) &&& (\<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b))
 2. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
 3. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
 4. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
 5. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))
 6. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)
[PROOF STEP]
show 1: "\<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x. x \<in> hom a b \<Longrightarrow> V_of_arr x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
[PROOF STEP]
fix a b f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x. x \<in> hom a b \<Longrightarrow> V_of_arr x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
[PROOF STEP]
assume f: "f \<in> hom a b"
[PROOF STATE]
proof (state)
this:
f \<in> hom a b

goal (1 subgoal):
 1. \<And>a b x. x \<in> hom a b \<Longrightarrow> V_of_arr x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
[PROOF STEP]
have "V_of_arr f = VLambda (V_of_ide (dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V_of_arr f = VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)
[PROOF STEP]
unfolding V_of_arr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) = VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V_of_arr f = VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<And>a b x. x \<in> hom a b \<Longrightarrow> V_of_arr x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V_of_arr f = VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<And>a b x. x \<in> hom a b \<Longrightarrow> V_of_arr x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
[PROOF STEP]
have "vfun (V_of_ide a) (V_of_ide b) ..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))
[PROOF STEP]
have "Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
assume x: "x \<in> elts (V_of_ide a)"
[PROOF STATE]
proof (state)
this:
x \<in> elts (V_of_ide a)

goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
have "(Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) x = Cls.DN (Cls.Fun f (Cls.UP x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x = Cls.DN (Cls.Fun f (Cls.arr_of x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x = Cls.DN (Cls.Fun f (Cls.arr_of x))

goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x = Cls.DN (Cls.Fun f (Cls.arr_of x))

goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
have "... \<in> elts (V_of_ide b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)
[PROOF STEP]
have "Cls.UP x \<in> Cls.Dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of x \<in> Cls.Dom f
[PROOF STEP]
by (metis (no_types, lifting) Cls.arr_dom_iff_arr Cls.arr_mkIde Cls.set_mkIde
                    bij_betw_ide_V(3) arr_char\<^sub>S\<^sub>b\<^sub>C dom_simp f ide_char\<^sub>S\<^sub>S\<^sub>C ide_of_V_def image_eqI
                    in_homE mem_Collect_eq x)
[PROOF STATE]
proof (state)
this:
Cls.arr_of x \<in> Cls.Dom f

goal (1 subgoal):
 1. Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)
[PROOF STEP]
hence "Cls.DN (Cls.Fun f (Cls.UP x)) \<in> Cls.DN ` Cls.Cod f"
[PROOF STATE]
proof (prove)
using this:
Cls.arr_of x \<in> Cls.Dom f

goal (1 subgoal):
 1. Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> Cls.DN ` Cls.Cod f
[PROOF STEP]
using f in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C arr_char\<^sub>S\<^sub>b\<^sub>C Cls.Fun_mapsto [of f]
[PROOF STATE]
proof (prove)
using this:
Cls.arr_of x \<in> Cls.Dom f
f \<in> hom a b
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)
arr ?f = (Cls.arr ?f \<and> (Cls.ide (Cls.dom ?f) \<and> Cls.Dom ?f \<subseteq> Cls.Univ \<and> small (Cls.Dom ?f)) \<and> Cls.ide (Cls.cod ?f) \<and> Cls.Cod ?f \<subseteq> Cls.Univ \<and> small (Cls.Cod ?f))
Cls.arr f \<Longrightarrow> Cls.Fun f \<in> extensional (Cls.Dom f) \<inter> (Cls.Dom f \<rightarrow> Cls.Cod f)

goal (1 subgoal):
 1. Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> Cls.DN ` Cls.Cod f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> Cls.DN ` Cls.Cod f

goal (1 subgoal):
 1. Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)
[PROOF STEP]
thus "Cls.DN (Cls.Fun f (Cls.UP x)) \<in> elts (V_of_ide b)"
[PROOF STATE]
proof (prove)
using this:
Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> Cls.DN ` Cls.Cod f

goal (1 subgoal):
 1. Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)
[PROOF STEP]
by (metis (no_types, lifting) V_of_ide_def arrE cod_char\<^sub>S\<^sub>b\<^sub>C elts_of_set f
                    in_homE mem_Collect_eq replacement)
[PROOF STATE]
proof (state)
this:
Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)

goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x = Cls.DN (Cls.Fun f (Cls.arr_of x))
Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)
[PROOF STEP]
show "(Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) x \<in> elts (V_of_ide b)"
[PROOF STATE]
proof (prove)
using this:
(Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x = Cls.DN (Cls.Fun f (Cls.arr_of x))
Cls.DN (Cls.Fun f (Cls.arr_of x)) \<in> elts (V_of_ide b)

goal (1 subgoal):
 1. (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)

goal (1 subgoal):
 1. vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)

goal (1 subgoal):
 1. vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))
[PROOF STEP]
using f vfunI
[PROOF STATE]
proof (prove)
using this:
Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)
f \<in> hom a b
?f \<in> elts ?A \<rightarrow> elts ?B \<Longrightarrow> vfun ?A ?B (VLambda ?A ?f)

goal (1 subgoal):
 1. vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))

goal (1 subgoal):
 1. \<And>a b x. x \<in> hom a b \<Longrightarrow> V_of_arr x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V_of_arr f = VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)
vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))
[PROOF STEP]
show "V_of_arr f \<in> Collect (vfun (V_of_ide a) (V_of_ide b))"
[PROOF STATE]
proof (prove)
using this:
V_of_arr f = VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)
vfun (V_of_ide a) (V_of_ide b) (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of))

goal (1 subgoal):
 1. V_of_arr f \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V_of_arr f \<in> Collect (vfun (V_of_ide a) (V_of_ide b))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
V_of_arr \<in> hom ?a1 ?b1 \<rightarrow> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1))

goal (5 subgoals):
 1. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
 2. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
 3. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
 4. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))
 5. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)
[PROOF STEP]
show 2: "\<And>a b. \<lbrakk>ide a; ide b\<rbrakk>
                        \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
[PROOF STEP]
assume a: "ide a" and b: "ide b"
[PROOF STATE]
proof (state)
this:
ide a
ide b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
[PROOF STEP]
show "arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<Longrightarrow> arr_of_V a b x \<in> hom a b
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<Longrightarrow> arr_of_V a b x \<in> hom a b
[PROOF STEP]
assume F: "F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))"
[PROOF STATE]
proof (state)
this:
F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))

goal (1 subgoal):
 1. \<And>x. x \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<Longrightarrow> arr_of_V a b x \<in> hom a b
[PROOF STEP]
have 3: "app F \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app F \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)
[PROOF STEP]
using F app_vfun_mapsto [of "V_of_ide a" "V_of_ide b" F]
[PROOF STATE]
proof (prove)
using this:
F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
vfun (V_of_ide a) (V_of_ide b) F \<Longrightarrow> app F \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)

goal (1 subgoal):
 1. app F \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
app F \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)

goal (1 subgoal):
 1. \<And>x. x \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<Longrightarrow> arr_of_V a b x \<in> hom a b
[PROOF STEP]
have 4: "app F \<in> Cls.DN ` (Cls.set a) \<rightarrow> Cls.DN ` (Cls.set b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app F \<in> Cls.DN ` Cls.set a \<rightarrow> Cls.DN ` Cls.set b
[PROOF STEP]
using 3 V_of_ide_def a b ide_char\<^sub>S\<^sub>S\<^sub>C
[PROOF STATE]
proof (prove)
using this:
app F \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)
V_of_ide ?a \<equiv> ZFC_in_HOL.set (Cls.DN ` Cls.set ?a)
ide a
ide b
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))

goal (1 subgoal):
 1. app F \<in> Cls.DN ` Cls.set a \<rightarrow> Cls.DN ` Cls.set b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
app F \<in> Cls.DN ` Cls.set a \<rightarrow> Cls.DN ` Cls.set b

goal (1 subgoal):
 1. \<And>x. x \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<Longrightarrow> arr_of_V a b x \<in> hom a b
[PROOF STEP]
have "arr_of_V a b F = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP \<circ> app F \<circ> Cls.DN)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_of_V a b F = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)
[PROOF STEP]
unfolding arr_of_V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
arr_of_V a b F = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)

goal (1 subgoal):
 1. \<And>x. x \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<Longrightarrow> arr_of_V a b x \<in> hom a b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arr_of_V a b F = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)

goal (1 subgoal):
 1. \<And>x. x \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<Longrightarrow> arr_of_V a b x \<in> hom a b
[PROOF STEP]
have "... \<in> hom a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN) \<in> hom a b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<guillemotleft>Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN) : a \<rightarrow> b\<guillemotright>
[PROOF STEP]
show "\<guillemotleft>Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP \<circ> app F \<circ> Cls.DN) : a \<rightarrow> b\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN) : a \<rightarrow> b\<guillemotright>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
 2. local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = a
 3. cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = b
[PROOF STEP]
have 4: "Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP \<circ> app F \<circ> Cls.DN))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
have "Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
[PROOF STEP]
using a b ide_char\<^sub>S\<^sub>S\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))

goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
have "Cls.UP \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
assume x: "x \<in> Cls.set a"
[PROOF STATE]
proof (state)
this:
x \<in> Cls.set a

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
have "(Cls.UP \<circ> app F \<circ> Cls.DN) x = Cls.UP (app F (Cls.DN x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
have "... \<in> Cls.set b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b
[PROOF STEP]
by (metis (no_types, lifting) 4 Cls.arr_mkIde Cls.ide_char' Cls.set_mkIde
                        PiE V_of_ide_def bij_betw_ide_V(3) b elts_of_set ide_char\<^sub>S\<^sub>S\<^sub>C
                        ide_of_V_def replacement rev_image_eqI x)
[PROOF STATE]
proof (state)
this:
Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))
Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b
[PROOF STEP]
show "(Cls.UP \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b"
[PROOF STATE]
proof (prove)
using this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))
Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b

goal (1 subgoal):
 1. (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr_of \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
Cls.arr_of \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
Cls.arr_of \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))

goal (3 subgoals):
 1. arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
 2. local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = a
 3. cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = b
[PROOF STEP]
show 5: "arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP \<circ> app F \<circ> Cls.DN))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
using a b 4 arr_char\<^sub>S\<^sub>b\<^sub>C ide_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
arr ?f = (Cls.arr ?f \<and> (Cls.ide (Cls.dom ?f) \<and> Cls.Dom ?f \<subseteq> Cls.Univ \<and> small (Cls.Dom ?f)) \<and> Cls.ide (Cls.cod ?f) \<and> Cls.Cod ?f \<subseteq> Cls.Univ \<and> small (Cls.Cod ?f))
ide ?a = (arr ?a \<and> Cls.ide ?a)

goal (1 subgoal):
 1. arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))

goal (2 subgoals):
 1. local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = a
 2. cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = b
[PROOF STEP]
show "dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP \<circ> app F \<circ> Cls.DN)) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = a
[PROOF STEP]
using a 4 5 dom_char\<^sub>S\<^sub>b\<^sub>C ide_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide a
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
local.dom ?f = (if arr ?f then Cls.dom ?f else Cls.null)
ide ?a = (arr ?a \<and> Cls.ide ?a)

goal (1 subgoal):
 1. local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = a

goal (1 subgoal):
 1. cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = b
[PROOF STEP]
show "cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP \<circ> app F \<circ> Cls.DN)) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = b
[PROOF STEP]
using b 4 5 cod_char\<^sub>S\<^sub>b\<^sub>C ide_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide b
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
cod ?f = (if arr ?f then Cls.cod ?f else Cls.null)
ide ?a = (arr ?a \<and> Cls.ide ?a)

goal (1 subgoal):
 1. cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cod (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<guillemotleft>Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN) : a \<rightarrow> b\<guillemotright>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN) \<in> hom a b

goal (1 subgoal):
 1. \<And>x. x \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<Longrightarrow> arr_of_V a b x \<in> hom a b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
arr_of_V a b F = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)
Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN) \<in> hom a b
[PROOF STEP]
show "arr_of_V a b F \<in> hom a b"
[PROOF STATE]
proof (prove)
using this:
arr_of_V a b F = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)
Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN) \<in> hom a b

goal (1 subgoal):
 1. arr_of_V a b F \<in> hom a b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arr_of_V a b F \<in> hom a b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>ide ?a1; ide ?b1\<rbrakk> \<Longrightarrow> arr_of_V ?a1 ?b1 \<in> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1)) \<rightarrow> hom ?a1 ?b1

goal (4 subgoals):
 1. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
 2. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
 3. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))
 4. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)
[PROOF STEP]
show 3: "\<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
fix a b f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
assume f: "f \<in> hom a b"
[PROOF STATE]
proof (state)
this:
f \<in> hom a b

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
have 4: "\<And>x. x \<in> Cls.set a
                        \<Longrightarrow> (Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN) x = Cls.Fun f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
assume x: "x \<in> Cls.set a"
[PROOF STATE]
proof (state)
this:
x \<in> Cls.set a

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
have "(Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN) x =
                Cls.UP (Cls.DN (Cls.Fun f (Cls.UP (Cls.DN x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.arr_of (Cls.DN (Cls.Fun f (Cls.arr_of (Cls.DN x))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.arr_of (Cls.DN (Cls.Fun f (Cls.arr_of (Cls.DN x))))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.arr_of (Cls.DN (Cls.Fun f (Cls.arr_of (Cls.DN x))))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
have "... = Cls.UP (Cls.DN (Cls.Fun f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of (Cls.DN (Cls.Fun f (Cls.arr_of (Cls.DN x)))) = Cls.arr_of (Cls.DN (Cls.Fun f x))
[PROOF STEP]
using x Cls.UP_DN
[PROOF STATE]
proof (prove)
using this:
x \<in> Cls.set a
?t \<in> range Cls.arr_of \<Longrightarrow> Cls.arr_of (Cls.DN ?t) = ?t

goal (1 subgoal):
 1. Cls.arr_of (Cls.DN (Cls.Fun f (Cls.arr_of (Cls.DN x)))) = Cls.arr_of (Cls.DN (Cls.Fun f x))
[PROOF STEP]
by (metis (no_types, lifting) Cls.elem_set_implies_incl_in Cls.incl_in_def
                Cls.setp_set_ide bij_betw_def replete_setcat.bij_arr_of subset_eq)
[PROOF STATE]
proof (state)
this:
Cls.arr_of (Cls.DN (Cls.Fun f (Cls.arr_of (Cls.DN x)))) = Cls.arr_of (Cls.DN (Cls.Fun f x))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Cls.arr_of (Cls.DN (Cls.Fun f (Cls.arr_of (Cls.DN x)))) = Cls.arr_of (Cls.DN (Cls.Fun f x))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
have "... = Cls.Fun f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of (Cls.DN (Cls.Fun f x)) = Cls.Fun f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.arr_of (Cls.DN (Cls.Fun f x)) = Cls.Fun f x
[PROOF STEP]
have "x \<in> Cls.Dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Cls.Dom f
[PROOF STEP]
using x f dom_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
x \<in> Cls.set a
f \<in> hom a b
local.dom ?f = (if arr ?f then Cls.dom ?f else Cls.null)

goal (1 subgoal):
 1. x \<in> Cls.Dom f
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<in> Cls.Dom f

goal (1 subgoal):
 1. Cls.arr_of (Cls.DN (Cls.Fun f x)) = Cls.Fun f x
[PROOF STEP]
hence "Cls.Fun f x \<in> Cls.Cod f"
[PROOF STATE]
proof (prove)
using this:
x \<in> Cls.Dom f

goal (1 subgoal):
 1. Cls.Fun f x \<in> Cls.Cod f
[PROOF STEP]
using x f Cls.Fun_mapsto in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
x \<in> Cls.Dom f
x \<in> Cls.set a
f \<in> hom a b
Cls.arr ?f \<Longrightarrow> Cls.Fun ?f \<in> extensional (Cls.Dom ?f) \<inter> (Cls.Dom ?f \<rightarrow> Cls.Cod ?f)
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)

goal (1 subgoal):
 1. Cls.Fun f x \<in> Cls.Cod f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.Fun f x \<in> Cls.Cod f

goal (1 subgoal):
 1. Cls.arr_of (Cls.DN (Cls.Fun f x)) = Cls.Fun f x
[PROOF STEP]
hence "Cls.Fun f x \<in> Cls.Univ"
[PROOF STATE]
proof (prove)
using this:
Cls.Fun f x \<in> Cls.Cod f

goal (1 subgoal):
 1. Cls.Fun f x \<in> Cls.Univ
[PROOF STEP]
using f cod_char\<^sub>S\<^sub>b\<^sub>C in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
Cls.Fun f x \<in> Cls.Cod f
f \<in> hom a b
cod ?f = (if arr ?f then Cls.cod ?f else Cls.null)
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)

goal (1 subgoal):
 1. Cls.Fun f x \<in> Cls.Univ
[PROOF STEP]
by (metis (no_types, lifting) Cls.elem_set_implies_incl_in Cls.incl_in_def
                  Cls.setp_set_ide subsetD)
[PROOF STATE]
proof (state)
this:
Cls.Fun f x \<in> Cls.Univ

goal (1 subgoal):
 1. Cls.arr_of (Cls.DN (Cls.Fun f x)) = Cls.Fun f x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Cls.Fun f x \<in> Cls.Univ

goal (1 subgoal):
 1. Cls.arr_of (Cls.DN (Cls.Fun f x)) = Cls.Fun f x
[PROOF STEP]
by (meson bij_betw_inv_into_right replete_setcat.bij_arr_of)
[PROOF STATE]
proof (state)
this:
Cls.arr_of (Cls.DN (Cls.Fun f x)) = Cls.Fun f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr_of (Cls.DN (Cls.Fun f x)) = Cls.Fun f x

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
show "(Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN) x = Cls.Fun f x"
[PROOF STATE]
proof (prove)
using this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x

goal (1 subgoal):
 1. (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x1 \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) ?x1 = Cls.Fun f ?x1

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
have 5: "Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b)
                                    (Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))
[PROOF STEP]
have "Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
[PROOF STEP]
using f ide_char\<^sub>S\<^sub>b\<^sub>C codomains_def domains_def in_hom_def
[PROOF STATE]
proof (prove)
using this:
f \<in> hom a b
ide ?a = (arr ?a \<and> Cls.ide ?a)
codomains ?f \<equiv> {b. ide b \<and> local.comp b ?f \<noteq> null}
domains ?f \<equiv> {a. ide a \<and> local.comp ?f a \<noteq> null}
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> \<equiv> ?a \<in> domains ?f \<and> ?b \<in> codomains ?f

goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))
[PROOF STEP]
have "Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN
                           \<in> Cls.set a \<rightarrow> Cls.set b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
assume x: "x \<in> Cls.set a"
[PROOF STATE]
proof (state)
this:
x \<in> Cls.set a

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
hence 6: "x \<in> Cls.Dom f"
[PROOF STATE]
proof (prove)
using this:
x \<in> Cls.set a

goal (1 subgoal):
 1. x \<in> Cls.Dom f
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
x \<in> Cls.set a
f \<in> hom a b

goal (1 subgoal):
 1. x \<in> Cls.Dom f
[PROOF STEP]
by (metis (no_types, lifting) dom_char\<^sub>S\<^sub>b\<^sub>C in_homE mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
x \<in> Cls.Dom f

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
have "(Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN) x = Cls.Fun f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
using 4 f x
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) ?x1 = Cls.Fun f ?x1
f \<in> hom a b
x \<in> Cls.set a

goal (1 subgoal):
 1. (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
have "... \<in> Cls.Cod f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.Fun f x \<in> Cls.Cod f
[PROOF STEP]
using 4 6 f Cls.Fun_mapsto
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) ?x1 = Cls.Fun f ?x1
x \<in> Cls.Dom f
f \<in> hom a b
Cls.arr ?f \<Longrightarrow> Cls.Fun ?f \<in> extensional (Cls.Dom ?f) \<inter> (Cls.Dom ?f \<rightarrow> Cls.Cod ?f)

goal (1 subgoal):
 1. Cls.Fun f x \<in> Cls.Cod f
[PROOF STEP]
by (metis (no_types, lifting) Cls.arr_dom_iff_arr Cls.elem_set_implies_incl_in
                  Cls.ideD(1) Cls.incl_in_def IntE PiE)
[PROOF STATE]
proof (state)
this:
Cls.Fun f x \<in> Cls.Cod f

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Cls.Fun f x \<in> Cls.Cod f

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
have "... = Cls.set b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.Cod f = Cls.set b
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f \<in> hom a b

goal (1 subgoal):
 1. Cls.Cod f = Cls.set b
[PROOF STEP]
by (metis (no_types, lifting) cod_char\<^sub>S\<^sub>b\<^sub>C in_homE mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
Cls.Cod f = Cls.set b

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
Cls.Fun f x \<in> Cls.Cod f
Cls.Cod f = Cls.set b
[PROOF STEP]
show "(Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN) x \<in> Cls.set b"
[PROOF STATE]
proof (prove)
using this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x = Cls.Fun f x
Cls.Fun f x \<in> Cls.Cod f
Cls.Cod f = Cls.set b

goal (1 subgoal):
 1. (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x \<in> Cls.set b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
have "arr_of_V a b (V_of_arr f) =
              Cls.mkArr (Cls.set a) (Cls.set b)
                        (Cls.UP \<circ> app (VLambda (V_of_ide (dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP))
                                \<circ> Cls.DN)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_of_V a b (V_of_arr f) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN)
[PROOF STEP]
unfolding arr_of_V_def V_of_arr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
arr_of_V a b (V_of_arr f) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN)

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
arr_of_V a b (V_of_arr f) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN)

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
have "... = Cls.mkArr (Cls.set a) (Cls.set b)
                                   (Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN)
[PROOF STEP]
proof (intro Cls.mkArr_eqI')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN))
 2. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
show 6: "\<And>x. x \<in> Cls.set a \<Longrightarrow>
                         (Cls.UP \<circ> app (VLambda (V_of_ide (dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP))
                                 \<circ> Cls.DN) x =
                         (Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
assume x: "x \<in> Cls.set a"
[PROOF STATE]
proof (state)
this:
x \<in> Cls.set a

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
have "(Cls.UP \<circ> app (VLambda (V_of_ide (dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP))
                          \<circ> Cls.DN) x =
                   Cls.UP (app (VLambda (V_of_ide (dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP))
                               (Cls.DN x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
have "... = (Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
have "Cls.DN x \<in> elts (V_of_ide (dom f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.DN x \<in> elts (V_of_ide (local.dom f))
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f \<in> hom a b

goal (1 subgoal):
 1. Cls.DN x \<in> elts (V_of_ide (local.dom f))
[PROOF STEP]
by (metis (no_types, lifting) V_of_ide_def elts_of_set ide_char\<^sub>S\<^sub>S\<^sub>C ide_dom image_eqI
                    in_homE mem_Collect_eq replacement x)
[PROOF STATE]
proof (state)
this:
Cls.DN x \<in> elts (V_of_ide (local.dom f))

goal (1 subgoal):
 1. Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Cls.DN x \<in> elts (V_of_ide (local.dom f))

goal (1 subgoal):
 1. Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
using beta
[PROOF STATE]
proof (prove)
using this:
Cls.DN x \<in> elts (V_of_ide (local.dom f))
?x \<in> elts ?A \<Longrightarrow> app (VLambda ?A ?b) ?x = ?b ?x

goal (1 subgoal):
 1. Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x))
Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
show "(Cls.UP \<circ> app (VLambda (V_of_ide (dom f))
                                                    (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP))
                                     \<circ> Cls.DN) x =
                             (Cls.UP \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP) \<circ> Cls.DN) x"
[PROOF STATE]
proof (prove)
using this:
(Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x))
Cls.arr_of (app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) (Cls.DN x)) = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x

goal (1 subgoal):
 1. (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) x = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x1 \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) ?x1 = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) ?x1

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN))
[PROOF STEP]
show "Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b)
                        (Cls.UP \<circ> app (VLambda (V_of_ide (local.dom f))
                                               (Cls.DN \<circ> Cls.Fun f \<circ> Cls.UP))
                                \<circ> Cls.DN))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN))
[PROOF STEP]
using 5 6 Cls.mkArr_eqI
[PROOF STATE]
proof (prove)
using this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))
?x1 \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) ?x1 = (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) ?x1
\<lbrakk>Cls.arr (Cls.mkArr ?A ?B ?F); ?A = ?A'; ?B = ?B'; \<And>x. x \<in> ?A \<Longrightarrow> ?F x = ?F' x\<rbrakk> \<Longrightarrow> Cls.mkArr ?A ?B ?F = Cls.mkArr ?A' ?B' ?F'

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN)

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app (VLambda (V_of_ide (local.dom f)) (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of)) \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN)

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
have "... = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f)
[PROOF STEP]
using 4 5
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) ?x1 = Cls.Fun f ?x1
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN))

goal (1 subgoal):
 1. Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f)

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> (Cls.DN \<circ> Cls.Fun f \<circ> Cls.arr_of) \<circ> Cls.DN) = Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f)

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
have "... = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f) = f
[PROOF STEP]
using f Cls.mkArr_Fun
[PROOF STATE]
proof (prove)
using this:
f \<in> hom a b
Cls.arr ?f \<Longrightarrow> Cls.mkArr (Cls.Dom ?f) (Cls.Cod ?f) (Cls.Fun ?f) = ?f

goal (1 subgoal):
 1. Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f) = f
[PROOF STEP]
by (metis (no_types, lifting) arr_char\<^sub>S\<^sub>b\<^sub>C cod_simp dom_char\<^sub>S\<^sub>b\<^sub>C in_homE mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
Cls.mkArr (Cls.set a) (Cls.set b) (Cls.Fun f) = f

goal (1 subgoal):
 1. \<And>a b f. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
show "arr_of_V a b (V_of_arr f) = f"
[PROOF STATE]
proof (prove)
using this:
arr_of_V a b (V_of_arr f) = f

goal (1 subgoal):
 1. arr_of_V a b (V_of_arr f) = f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
arr_of_V a b (V_of_arr f) = f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f1 \<in> hom ?a1 ?b1 \<Longrightarrow> arr_of_V ?a1 ?b1 (V_of_arr ?f1) = ?f1

goal (3 subgoals):
 1. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
 2. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))
 3. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)
[PROOF STEP]
show 4: "\<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk>
                          \<Longrightarrow> V_of_arr (arr_of_V a b F) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
fix a b F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
assume a: "ide a" and b: "ide b"
[PROOF STATE]
proof (state)
this:
ide a
ide b

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
assume F: "F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))"
[PROOF STATE]
proof (state)
this:
F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
have "F \<in> elts (VPow (vtimes (V_of_ide a) (V_of_ide b))) \<and>
              elts (V_of_ide a) = Domain (pairs F) \<and> single_valued (pairs F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> elts (VPow (vtimes (V_of_ide a) (V_of_ide b))) \<and> elts (V_of_ide a) = Domain (pairs F) \<and> single_valued (pairs F)
[PROOF STEP]
using F vfun_def
[PROOF STATE]
proof (prove)
using this:
F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
vfun ?A ?B ?f \<equiv> ?f \<in> elts (VPow (vtimes ?A ?B)) \<and> elts ?A = Domain (pairs ?f) \<and> single_valued (pairs ?f)

goal (1 subgoal):
 1. F \<in> elts (VPow (vtimes (V_of_ide a) (V_of_ide b))) \<and> elts (V_of_ide a) = Domain (pairs F) \<and> single_valued (pairs F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F \<in> elts (VPow (vtimes (V_of_ide a) (V_of_ide b))) \<and> elts (V_of_ide a) = Domain (pairs F) \<and> single_valued (pairs F)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
hence 5: "F \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))"
[PROOF STATE]
proof (prove)
using this:
F \<in> elts (VPow (vtimes (V_of_ide a) (V_of_ide b))) \<and> elts (V_of_ide a) = Domain (pairs F) \<and> single_valued (pairs F)

goal (1 subgoal):
 1. F \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
[PROOF STEP]
unfolding VPi_def
[PROOF STATE]
proof (prove)
using this:
F \<in> elts (VPow (vtimes (V_of_ide a) (V_of_ide b))) \<and> elts (V_of_ide a) = Domain (pairs F) \<and> single_valued (pairs F)

goal (1 subgoal):
 1. F \<in> elts (ZFC_in_HOL.set {f \<in> elts (VPow (vtimes (V_of_ide a) (V_of_ide b))). elts (V_of_ide a) \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)})
[PROOF STEP]
by (metis (no_types, lifting) down elts_of_set mem_Collect_eq subsetI)
[PROOF STATE]
proof (state)
this:
F \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
let ?f = "Cls.mkArr (Cls.set a) (Cls.set b) (Cls.UP \<circ> app F \<circ> Cls.DN)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
have 6: "Cls.arr ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
have "Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
[PROOF STEP]
using a b ide_char\<^sub>S\<^sub>S\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))

goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
have "Cls.UP \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
assume x: "x \<in> Cls.set a"
[PROOF STATE]
proof (state)
this:
x \<in> Cls.set a

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
have "(Cls.UP \<circ> app F \<circ> Cls.DN) x = Cls.UP (app F (Cls.DN x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
have "... \<in> Cls.set b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b
[PROOF STEP]
have "app F (Cls.DN x) \<in> Cls.DN ` Cls.set b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app F (Cls.DN x) \<in> Cls.DN ` Cls.set b
[PROOF STEP]
using a b ide_char\<^sub>S\<^sub>S\<^sub>C x F app_vfun_mapsto [of "V_of_ide a" "V_of_ide b" F]
                      V_of_ide_def
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))
x \<in> Cls.set a
F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))
vfun (V_of_ide a) (V_of_ide b) F \<Longrightarrow> app F \<in> elts (V_of_ide a) \<rightarrow> elts (V_of_ide b)
V_of_ide ?a \<equiv> ZFC_in_HOL.set (Cls.DN ` Cls.set ?a)

goal (1 subgoal):
 1. app F (Cls.DN x) \<in> Cls.DN ` Cls.set b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
app F (Cls.DN x) \<in> Cls.DN ` Cls.set b

goal (1 subgoal):
 1. Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
app F (Cls.DN x) \<in> Cls.DN ` Cls.set b

goal (1 subgoal):
 1. Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b
[PROOF STEP]
using \<open>Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ\<close>
[PROOF STATE]
proof (prove)
using this:
app F (Cls.DN x) \<in> Cls.DN ` Cls.set b
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b
[PROOF STEP]
by (metis Cls.bij_arr_of bij_betw_def imageI image_inv_into_cancel)
[PROOF STATE]
proof (state)
this:
Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))
Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b
[PROOF STEP]
show "(Cls.UP \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b"
[PROOF STATE]
proof (prove)
using this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x = Cls.arr_of (app F (Cls.DN x))
Cls.arr_of (app F (Cls.DN x)) \<in> Cls.set b

goal (1 subgoal):
 1. (Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Cls.arr_of \<circ> app F \<circ> Cls.DN) x \<in> Cls.set b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr_of \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
Cls.arr_of \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Cls.set a \<subseteq> Cls.Univ \<and> Cls.set b \<subseteq> Cls.Univ
Cls.arr_of \<circ> app F \<circ> Cls.DN \<in> Cls.set a \<rightarrow> Cls.set b

goal (1 subgoal):
 1. Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
have "V_of_arr (arr_of_V a b F) = VLambda (V_of_ide (dom ?f)) (Cls.DN \<circ> Cls.Fun ?f \<circ> Cls.UP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V_of_arr (arr_of_V a b F) = VLambda (V_of_ide (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)
[PROOF STEP]
unfolding V_of_arr_def arr_of_V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (V_of_ide (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (V_of_ide (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V_of_arr (arr_of_V a b F) = VLambda (V_of_ide (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
V_of_arr (arr_of_V a b F) = VLambda (V_of_ide (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
have "... = VLambda (V_of_ide a) (Cls.DN \<circ> Cls.Fun ?f \<circ> Cls.UP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (V_of_ide (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)
[PROOF STEP]
unfolding V_of_ide_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (ZFC_in_HOL.set (Cls.DN ` Cls.set (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (ZFC_in_HOL.set (Cls.DN ` Cls.set a)) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)
[PROOF STEP]
using a b 6 ide_char\<^sub>S\<^sub>S\<^sub>C V_of_ide_def dom_char\<^sub>S\<^sub>b\<^sub>C Cls.dom_mkArr arrI\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))
V_of_ide ?a \<equiv> ZFC_in_HOL.set (Cls.DN ` Cls.set ?a)
local.dom ?f = (if arr ?f then Cls.dom ?f else Cls.null)
Cls.arr (Cls.mkArr ?A ?B ?F) \<Longrightarrow> Cls.dom (Cls.mkArr ?A ?B ?F) = Cls.mkIde ?A
Cls.arr ?f \<and> (Cls.ide (Cls.dom ?f) \<and> Cls.Dom ?f \<subseteq> Cls.Univ \<and> small (Cls.Dom ?f)) \<and> Cls.ide (Cls.cod ?f) \<and> Cls.Cod ?f \<subseteq> Cls.Univ \<and> small (Cls.Cod ?f) \<Longrightarrow> arr ?f

goal (1 subgoal):
 1. VLambda (ZFC_in_HOL.set (Cls.DN ` Cls.set (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (ZFC_in_HOL.set (Cls.DN ` Cls.set a)) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide (local.dom (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)))) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
have "... = VLambda (V_of_ide a)
                                 (Cls.DN \<circ>
                                    restrict (Cls.UP \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.UP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)
[PROOF STEP]
using 6 Cls.Fun_mkArr
[PROOF STATE]
proof (prove)
using this:
Cls.arr (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN))
Cls.arr (Cls.mkArr ?A ?B ?F) \<Longrightarrow> Cls.Fun (Cls.mkArr ?A ?B ?F) = restrict ?F ?A

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (Cls.DN \<circ> Cls.Fun (Cls.mkArr (Cls.set a) (Cls.set b) (Cls.arr_of \<circ> app F \<circ> Cls.DN)) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
have "... = VLambda (V_of_ide a) (app F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
have 7: "\<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow>
                         (Cls.DN \<circ> restrict (Cls.UP \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.UP) x =
                         app F x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) x = app F x
[PROOF STEP]
unfolding V_of_ide_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a)) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) x = app F x
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
ide a

goal (1 subgoal):
 1. \<And>x. x \<in> elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a)) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) x = app F x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> (if small (Cls.DN ` Cls.set a) then Cls.DN ` Cls.set a else {}); partial_magma.ide (subcategory.comp Cls.comp (\<lambda>f. Cls.arr f \<and> Cls.ide (Cls.dom f) \<and> Cls.Dom f \<subseteq> Cls.Univ \<and> small (Cls.Dom f) \<and> Cls.ide (Cls.cod f) \<and> Cls.Cod f \<subseteq> Cls.Univ \<and> small (Cls.Cod f))) a\<rbrakk> \<Longrightarrow> Cls.arr_of x \<notin> Cls.set a \<longrightarrow> Cls.DN undefined = app F x
[PROOF STEP]
by (metis (no_types, lifting) Cls.bij_arr_of a bij_betw_def empty_iff ide_char\<^sub>S\<^sub>S\<^sub>C
                image_eqI image_inv_into_cancel)
[PROOF STATE]
proof (state)
this:
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) ?x1 = app F ?x1

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
have 8: "\<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow>
                         (Cls.DN \<circ> restrict (Cls.UP \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.UP) x
                            \<in> elts (V_of_ide b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
using 5 7 VPi_D
[PROOF STATE]
proof (prove)
using this:
F \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) ?x1 = app F ?x1
\<lbrakk>?f \<in> elts (VPi ?A ?B); ?x \<in> elts ?A\<rbrakk> \<Longrightarrow> app ?f ?x \<in> elts (?B ?x)

goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) x \<in> elts (V_of_ide b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) ?x1 \<in> elts (V_of_ide b)

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
have "VLambda (V_of_ide a) (app F) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (V_of_ide a) (app F) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
[PROOF STEP]
using 5 VPi_I VPi_D
[PROOF STATE]
proof (prove)
using this:
F \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
(\<And>x. x \<in> elts ?A \<Longrightarrow> ?b x \<in> elts (?B x)) \<Longrightarrow> VLambda ?A ?b \<in> elts (VPi ?A ?B)
\<lbrakk>?f \<in> elts (VPi ?A ?B); ?x \<in> elts ?A\<rbrakk> \<Longrightarrow> app ?f ?x \<in> elts (?B ?x)

goal (1 subgoal):
 1. VLambda (V_of_ide a) (app F) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (app F) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (app F) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
have "VLambda (V_of_ide a)
                                 (Cls.DN \<circ>
                                    restrict (Cls.UP \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.UP)
                           \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
[PROOF STEP]
using 8 VPi_I
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) ?x1 \<in> elts (V_of_ide b)
(\<And>x. x \<in> elts ?A \<Longrightarrow> ?b x \<in> elts (?B x)) \<Longrightarrow> VLambda ?A ?b \<in> elts (VPi ?A ?B)

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
have "\<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow>
                               app (VLambda (V_of_ide a)
                                   (Cls.DN \<circ>
                                      restrict (Cls.UP \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ>
                                        Cls.UP)) x =
                               app F x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> app (VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)) x = app F x
[PROOF STEP]
using 7 beta
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) ?x1 = app F ?x1
?x \<in> elts ?A \<Longrightarrow> app (VLambda ?A ?b) ?x = ?b ?x

goal (1 subgoal):
 1. \<And>x. x \<in> elts (V_of_ide a) \<Longrightarrow> app (VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)) x = app F x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> app (VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)) ?x1 = app F ?x1

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
VLambda (V_of_ide a) (app F) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> app (VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)) ?x1 = app F ?x1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
VLambda (V_of_ide a) (app F) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> app (VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)) ?x1 = app F ?x1

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
using fun_ext
[PROOF STATE]
proof (prove)
using this:
VLambda (V_of_ide a) (app F) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
?x1 \<in> elts (V_of_ide a) \<Longrightarrow> app (VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of)) ?x1 = app F ?x1
\<lbrakk>?f \<in> elts (VPi ?A ?B); ?g \<in> elts (VPi ?A ?B); \<And>x. x \<in> elts ?A \<Longrightarrow> app ?f x = app ?g x\<rbrakk> \<Longrightarrow> ?f = ?g

goal (1 subgoal):
 1. VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (Cls.DN \<circ> restrict (Cls.arr_of \<circ> app F \<circ> Cls.DN) (Cls.set a) \<circ> Cls.arr_of) = VLambda (V_of_ide a) (app F)

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
have "... = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (V_of_ide a) (app F) = F
[PROOF STEP]
using 5 eta [of F "V_of_ide a" "\<lambda>_. V_of_ide b"]
[PROOF STATE]
proof (prove)
using this:
F \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b))
F \<in> elts (VPi (V_of_ide a) (\<lambda>_. V_of_ide b)) \<Longrightarrow> VLambda (V_of_ide a) (app F) = F

goal (1 subgoal):
 1. VLambda (V_of_ide a) (app F) = F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VLambda (V_of_ide a) (app F) = F

goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
show "V_of_arr (arr_of_V a b F) = F"
[PROOF STATE]
proof (prove)
using this:
V_of_arr (arr_of_V a b F) = F

goal (1 subgoal):
 1. V_of_arr (arr_of_V a b F) = F
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V_of_arr (arr_of_V a b F) = F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>ide ?a1; ide ?b1; ?F1 \<in> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V ?a1 ?b1 ?F1) = ?F1

goal (2 subgoals):
 1. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))
 2. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)
[PROOF STEP]
show "\<lbrakk>ide a; ide b\<rbrakk>
               \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))
[PROOF STEP]
using 1 2 3 4
[PROOF STATE]
proof (prove)
using this:
V_of_arr \<in> hom ?a1 ?b1 \<rightarrow> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1))
\<lbrakk>ide ?a1; ide ?b1\<rbrakk> \<Longrightarrow> arr_of_V ?a1 ?b1 \<in> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1)) \<rightarrow> hom ?a1 ?b1
?f1 \<in> hom ?a1 ?b1 \<Longrightarrow> arr_of_V ?a1 ?b1 (V_of_arr ?f1) = ?f1
\<lbrakk>ide ?a1; ide ?b1; ?F1 \<in> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V ?a1 ?b1 ?F1) = ?F1

goal (1 subgoal):
 1. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))
[PROOF STEP]
apply (intro bij_betwI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F\<rbrakk> \<Longrightarrow> V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b))
 2. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F\<rbrakk> \<Longrightarrow> ?g12 \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
 3. \<And>x. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; x \<in> hom a b\<rbrakk> \<Longrightarrow> ?g12 (V_of_arr x) = x
 4. \<And>y. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; y \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (?g12 y) = y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F\<rbrakk> \<Longrightarrow> ?g12 \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
 2. \<And>x. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; x \<in> hom a b\<rbrakk> \<Longrightarrow> ?g12 (V_of_arr x) = x
 3. \<And>y. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; y \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (?g12 y) = y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; x \<in> hom a b\<rbrakk> \<Longrightarrow> arr_of_V a b (V_of_arr x) = x
 2. \<And>y. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; y \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b y) = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom a b) (Collect (vfun (V_of_ide a) (V_of_ide b)))

goal (1 subgoal):
 1. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)
[PROOF STEP]
show "\<lbrakk>ide a; ide b\<rbrakk>
               \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)
[PROOF STEP]
using 1 2 3 4
[PROOF STATE]
proof (prove)
using this:
V_of_arr \<in> hom ?a1 ?b1 \<rightarrow> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1))
\<lbrakk>ide ?a1; ide ?b1\<rbrakk> \<Longrightarrow> arr_of_V ?a1 ?b1 \<in> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1)) \<rightarrow> hom ?a1 ?b1
?f1 \<in> hom ?a1 ?b1 \<Longrightarrow> arr_of_V ?a1 ?b1 (V_of_arr ?f1) = ?f1
\<lbrakk>ide ?a1; ide ?b1; ?F1 \<in> Collect (vfun (V_of_ide ?a1) (V_of_ide ?b1))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V ?a1 ?b1 ?F1) = ?F1

goal (1 subgoal):
 1. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)
[PROOF STEP]
apply (intro bij_betwI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b
 2. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F\<rbrakk> \<Longrightarrow> ?g12 \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b))
 3. \<And>x. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> ?g12 (arr_of_V a b x) = x
 4. \<And>y. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; y \<in> hom a b\<rbrakk> \<Longrightarrow> arr_of_V a b (?g12 y) = y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F\<rbrakk> \<Longrightarrow> ?g12 \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b))
 2. \<And>x. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> ?g12 (arr_of_V a b x) = x
 3. \<And>y. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; y \<in> hom a b\<rbrakk> \<Longrightarrow> arr_of_V a b (?g12 y) = y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; x \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b x) = x
 2. \<And>y. \<lbrakk>ide a; ide b; \<And>a b. V_of_arr \<in> hom a b \<rightarrow> Collect (vfun (V_of_ide a) (V_of_ide b)); \<And>a b. \<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> arr_of_V a b \<in> Collect (vfun (V_of_ide a) (V_of_ide b)) \<rightarrow> hom a b; \<And>f a b. f \<in> hom a b \<Longrightarrow> arr_of_V a b (V_of_arr f) = f; \<And>a b F. \<lbrakk>ide a; ide b; F \<in> Collect (vfun (V_of_ide a) (V_of_ide b))\<rbrakk> \<Longrightarrow> V_of_arr (arr_of_V a b F) = F; y \<in> hom a b\<rbrakk> \<Longrightarrow> arr_of_V a b (V_of_arr y) = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>ide a; ide b\<rbrakk> \<Longrightarrow> bij_betw (arr_of_V a b) (Collect (vfun (V_of_ide a) (V_of_ide b))) (hom a b)

goal:
No subgoals!
[PROOF STEP]
qed