[STATEMENT]
lemma ordinal_composableI[cat_ordinal_cs_intros]:
  assumes "x = [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ>"
    and "a \<in>\<^sub>\<circ> A"
    and "b \<in>\<^sub>\<circ> A"
    and "c \<in>\<^sub>\<circ> A"
    and "a \<le> b"
    and "b \<le> c"
  shows "x \<in>\<^sub>\<circ> ordinal_composable A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x = [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
b \<subseteq>\<^sub>\<circ> c

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
by auto


[STATEMENT]
lemma ordinal_composableD[dest]:
  assumes "[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> \<in>\<^sub>\<circ> ordinal_composable A"
  shows "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> A" and "c \<in>\<^sub>\<circ> A" and "a \<le> b" and "b \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A) &&& c \<in>\<^sub>\<circ> A &&& a \<subseteq>\<^sub>\<circ> b &&& b \<subseteq>\<^sub>\<circ> c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}

goal (1 subgoal):
 1. (a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A) &&& c \<in>\<^sub>\<circ> A &&& a \<subseteq>\<^sub>\<circ> b &&& b \<subseteq>\<^sub>\<circ> c
[PROOF STEP]
by auto


[STATEMENT]
lemma ordinal_composableE[elim]:
  assumes "x \<in>\<^sub>\<circ> ordinal_composable A"
  obtains a b c
    where "x = [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ>"
      and "a \<in>\<^sub>\<circ> A"
      and "b \<in>\<^sub>\<circ> A"
      and "c \<in>\<^sub>\<circ> A"
      and "a \<le> b"
      and "b \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b c a. \<lbrakk>x = [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ>; a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> A; c \<in>\<^sub>\<circ> A; a \<subseteq>\<^sub>\<circ> b; b \<subseteq>\<^sub>\<circ> c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}

goal (1 subgoal):
 1. (\<And>b c a. \<lbrakk>x = [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ>; a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> A; c \<in>\<^sub>\<circ> A; a \<subseteq>\<^sub>\<circ> b; b \<subseteq>\<^sub>\<circ> c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma cat_ordinal_components:
  shows [cat_ordinal_cs_simps]: "cat_ordinal A\<lparr>Obj\<rparr> = A"
    and [cat_ordinal_cs_simps]: "cat_ordinal A\<lparr>Arr\<rparr> = ordinal_arrs A"
    and "cat_ordinal A\<lparr>Dom\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>0\<rparr>)"
    and "cat_ordinal A\<lparr>Cod\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>)"
    and "cat_ordinal A\<lparr>Comp\<rparr> =
      (\<lambda>gf\<in>\<^sub>\<circ>ordinal_composable A. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>0\<rparr>, gf\<lparr>0\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>)"
    and "cat_ordinal A\<lparr>CId\<rparr> = (\<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cat_ordinal A\<lparr>Obj\<rparr> = A &&& cat_ordinal A\<lparr>Arr\<rparr> = ordinal_arrs A &&& cat_ordinal A\<lparr>Dom\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>)) &&& cat_ordinal A\<lparr>Cod\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>) &&& cat_ordinal A\<lparr>Comp\<rparr> = (\<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>) &&& cat_ordinal A\<lparr>CId\<rparr> = (\<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>)
[PROOF STEP]
unfolding cat_ordinal_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([A, ordinal_arrs A, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = A &&& [A, ordinal_arrs A, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = ordinal_arrs A &&& [A, ordinal_arrs A, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>)) &&& [A, ordinal_arrs A, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>) &&& [A, ordinal_arrs A, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = (\<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>) &&& [A, ordinal_arrs A, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>5\<^sub>\<nat>\<rparr> = (\<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>)
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma cat_ordinal_Dom_app[cat_ordinal_cs_simps]:
  assumes "x \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Arr\<rparr>" and "x = [a, b]\<^sub>\<circ>"
  shows "cat_ordinal A\<lparr>Dom\<rparr>\<lparr>x\<rparr> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_ordinal A\<lparr>Dom\<rparr>\<lparr>x\<rparr> = a
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. cat_ordinal A\<lparr>Dom\<rparr>\<lparr>x\<rparr> = a
[PROOF STEP]
unfolding assms(2) cat_ordinal_components
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> ordinal_arrs A

goal (1 subgoal):
 1. (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>) \<lparr>a, b\<rparr>\<^sub>\<bullet> = a
[PROOF STEP]
by auto


[STATEMENT]
lemma cat_ordinal_Dom_vrange: "\<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>) \<subseteq>\<^sub>\<circ> A
[PROOF STEP]
by (intro vrange_VLambda_vsubset, elim ordinal_arrsE) simp


[STATEMENT]
lemma cat_ordinal_Cod_app[cat_ordinal_cs_simps]:
  assumes "x \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Arr\<rparr>" and "x = [a, b]\<^sub>\<circ>"
  shows "cat_ordinal A\<lparr>Cod\<rparr>\<lparr>x\<rparr> = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_ordinal A\<lparr>Cod\<rparr>\<lparr>x\<rparr> = b
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. cat_ordinal A\<lparr>Cod\<rparr>\<lparr>x\<rparr> = b
[PROOF STEP]
unfolding assms(2) cat_ordinal_components
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> ordinal_arrs A

goal (1 subgoal):
 1. (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>) \<lparr>a, b\<rparr>\<^sub>\<bullet> = b
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma cat_ordinal_Cod_vrange: "\<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>) \<subseteq>\<^sub>\<circ> A
[PROOF STEP]
by (intro vrange_VLambda_vsubset, elim ordinal_arrsE)
    (simp add: nat_omega_simps)


[STATEMENT]
lemma cat_ordinal_is_arrI[cat_ordinal_cs_intros]:
  assumes "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> A" and "a \<le> b" and "f = [a, b]\<^sub>\<circ>"
  shows "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
proof(intro is_arrI, unfold cat_ordinal_components(2))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in>\<^sub>\<circ> ordinal_arrs A
 2. cat_ordinal A\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 3. cat_ordinal A\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>
[PROOF STEP]
show "f \<in>\<^sub>\<circ> ordinal_arrs A"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> ordinal_arrs A
[PROOF STEP]
by (intro ordinal_arrsI)
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> ordinal_arrs A

goal (2 subgoals):
 1. cat_ordinal A\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 2. cat_ordinal A\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> ordinal_arrs A
[PROOF STEP]
show "cat_ordinal A\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a" "cat_ordinal A\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> ordinal_arrs A

goal (1 subgoal):
 1. cat_ordinal A\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a &&& cat_ordinal A\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
by (cs_concl cs_simp: cat_ordinal_cs_simps assms(4))+
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
cat_ordinal A\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_ordinal_is_arrD[dest]:
  assumes "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
  shows "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> A" and "a \<le> b" and "f = [a, b]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A) &&& a \<subseteq>\<^sub>\<circ> b &&& f = [a, b]\<^sub>\<circ>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. a \<in>\<^sub>\<circ> A
 2. b \<in>\<^sub>\<circ> A
 3. a \<subseteq>\<^sub>\<circ> b
 4. f = [a, b]\<^sub>\<circ>
[PROOF STEP]
note f = is_arrD[OF assms, unfolded cat_ordinal_components(2)]
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> ordinal_arrs A
cat_ordinal A\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
cat_ordinal A\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b

goal (4 subgoals):
 1. a \<in>\<^sub>\<circ> A
 2. b \<in>\<^sub>\<circ> A
 3. a \<subseteq>\<^sub>\<circ> b
 4. f = [a, b]\<^sub>\<circ>
[PROOF STEP]
from f(1)
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> ordinal_arrs A
[PROOF STEP]
obtain a' b'
    where a': "a' \<in>\<^sub>\<circ> A"
      and b': "b' \<in>\<^sub>\<circ> A"
      and a'b': "a' \<le> b'"
      and f_def: "f = [a', b']\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> ordinal_arrs A

goal (1 subgoal):
 1. (\<And>a' b'. \<lbrakk>a' \<in>\<^sub>\<circ> A; b' \<in>\<^sub>\<circ> A; a' \<subseteq>\<^sub>\<circ> b'; f = [a', b']\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ordinal_arrs_def
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> ZFC_in_HOL.set {[a, b]\<^sub>\<circ> |a b. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b}

goal (1 subgoal):
 1. (\<And>a' b'. \<lbrakk>a' \<in>\<^sub>\<circ> A; b' \<in>\<^sub>\<circ> A; a' \<subseteq>\<^sub>\<circ> b'; f = [a', b']\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
a' \<in>\<^sub>\<circ> A
b' \<in>\<^sub>\<circ> A
a' \<subseteq>\<^sub>\<circ> b'
f = [a', b']\<^sub>\<circ>

goal (4 subgoals):
 1. a \<in>\<^sub>\<circ> A
 2. b \<in>\<^sub>\<circ> A
 3. a \<subseteq>\<^sub>\<circ> b
 4. f = [a, b]\<^sub>\<circ>
[PROOF STEP]
from f(2) a' b' a'b'
[PROOF STATE]
proof (chain)
picking this:
cat_ordinal A\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
a' \<in>\<^sub>\<circ> A
b' \<in>\<^sub>\<circ> A
a' \<subseteq>\<^sub>\<circ> b'
[PROOF STEP]
have a'_def: "a' = a"
[PROOF STATE]
proof (prove)
using this:
cat_ordinal A\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
a' \<in>\<^sub>\<circ> A
b' \<in>\<^sub>\<circ> A
a' \<subseteq>\<^sub>\<circ> b'

goal (1 subgoal):
 1. a' = a
[PROOF STEP]
by
      (
        cs_prems cs_shallow
          cs_simp: cat_ordinal_cs_simps f_def cs_intro: cat_ordinal_cs_intros
      )
[PROOF STATE]
proof (state)
this:
a' = a

goal (4 subgoals):
 1. a \<in>\<^sub>\<circ> A
 2. b \<in>\<^sub>\<circ> A
 3. a \<subseteq>\<^sub>\<circ> b
 4. f = [a, b]\<^sub>\<circ>
[PROOF STEP]
from f(3) a' b' a'b'
[PROOF STATE]
proof (chain)
picking this:
cat_ordinal A\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
a' \<in>\<^sub>\<circ> A
b' \<in>\<^sub>\<circ> A
a' \<subseteq>\<^sub>\<circ> b'
[PROOF STEP]
have b'_def: "b' = b"
[PROOF STATE]
proof (prove)
using this:
cat_ordinal A\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
a' \<in>\<^sub>\<circ> A
b' \<in>\<^sub>\<circ> A
a' \<subseteq>\<^sub>\<circ> b'

goal (1 subgoal):
 1. b' = b
[PROOF STEP]
by
      (
        cs_prems cs_shallow
          cs_simp: cat_ordinal_cs_simps f_def cs_intro: cat_ordinal_cs_intros
      )
[PROOF STATE]
proof (state)
this:
b' = b

goal (4 subgoals):
 1. a \<in>\<^sub>\<circ> A
 2. b \<in>\<^sub>\<circ> A
 3. a \<subseteq>\<^sub>\<circ> b
 4. f = [a, b]\<^sub>\<circ>
[PROOF STEP]
from a' b' a'b' f_def
[PROOF STATE]
proof (chain)
picking this:
a' \<in>\<^sub>\<circ> A
b' \<in>\<^sub>\<circ> A
a' \<subseteq>\<^sub>\<circ> b'
f = [a', b']\<^sub>\<circ>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> A" and "a \<le> b" and "f = [a, b]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
a' \<in>\<^sub>\<circ> A
b' \<in>\<^sub>\<circ> A
a' \<subseteq>\<^sub>\<circ> b'
f = [a', b']\<^sub>\<circ>

goal (1 subgoal):
 1. (a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A) &&& a \<subseteq>\<^sub>\<circ> b &&& f = [a, b]\<^sub>\<circ>
[PROOF STEP]
unfolding a'_def b'_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. (a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A) &&& a \<subseteq>\<^sub>\<circ> b &&& f = [a, b]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_ordinal_is_arrE[elim]:
  assumes "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
  obtains "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> A" and "a \<le> b" and "f = [a, b]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> A; a \<subseteq>\<^sub>\<circ> b; f = [a, b]\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. (\<lbrakk>a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> A; a \<subseteq>\<^sub>\<circ> b; f = [a, b]\<^sub>\<circ>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma cat_ordinal_is_arr_not:
  assumes "\<not>a \<le> b"
  shows "\<not>f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
proof(rule ccontr, unfold not_not)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> False
[PROOF STEP]
assume "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> False
[PROOF STEP]
with cat_ordinal_is_arrD(3)[OF this] assms
[PROOF STATE]
proof (chain)
picking this:
a \<subseteq>\<^sub>\<circ> b
\<not> a \<subseteq>\<^sub>\<circ> b
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
a \<subseteq>\<^sub>\<circ> b
\<not> a \<subseteq>\<^sub>\<circ> b
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_ordinal_is_arr_is_unique:
  assumes "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b" and "g : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
  shows "f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g
[PROOF STEP]
by
    (
      simp add:
        cat_ordinal_is_arrD(4)[OF assms(1)]
        cat_ordinal_is_arrD(4)[OF assms(2)]
    )


[STATEMENT]
lemma cat_ordinal_Hom_ne:
  assumes "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
  shows "Hom (cat_ordinal A) a b = set {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}
[PROOF STEP]
using assms cat_ordinal_is_arr_is_unique
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
\<lbrakk>?f : ?a \<mapsto>\<^bsub>cat_ordinal ?A\<^esub> ?b; ?g : ?a \<mapsto>\<^bsub>cat_ordinal ?A\<^esub> ?b\<rbrakk> \<Longrightarrow> ?f = ?g

goal (1 subgoal):
 1. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}
[PROOF STEP]
by (intro vsubset_antisym vsubsetI) auto


[STATEMENT]
lemma cat_ordinal_Hom_empty:
  assumes "\<not>a \<le> b"
  shows "Hom (cat_ordinal A) a b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
by (intro vsubset_antisym vsubsetI) auto


[STATEMENT]
lemma cat_ordinal_inj:
  assumes "cat_ordinal m = cat_ordinal n"
  shows "m = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = n
[PROOF STEP]
by (metis assms cat_ordinal_components(1))


[STATEMENT]
lemma cat_ordinal_Comp_app[cat_ordinal_cs_simps]:
  assumes "g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c" and "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
  shows "g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
have a: "a \<in>\<^sub>\<circ> A"
    and b: "b \<in>\<^sub>\<circ> A"
    and ab: "a \<le> b"
    and f_def: "f = [a, b]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. (a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A) &&& a \<subseteq>\<^sub>\<circ> b &&& f = [a, b]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
[PROOF STEP]
have c: "c \<in>\<^sub>\<circ> A" and bc: "b \<le> c" and g_def: "g = [b, c]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c

goal (1 subgoal):
 1. c \<in>\<^sub>\<circ> A &&& b \<subseteq>\<^sub>\<circ> c &&& g = [b, c]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
g = [b, c]\<^sub>\<circ>

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>
[PROOF STEP]
from a b c ab bc
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
b \<subseteq>\<^sub>\<circ> c
[PROOF STEP]
have "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> ordinal_composable A"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
b \<subseteq>\<^sub>\<circ> c

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: g_def f_def cs_intro: cat_ordinal_cs_intros)
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
show "g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}

goal (1 subgoal):
 1. (\<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>) \<lparr>g, f\<rparr>\<^sub>\<bullet> = [a, c]\<^sub>\<circ>
[PROOF STEP]
by (simp add: g_def f_def nat_omega_simps)
[PROOF STATE]
proof (state)
this:
g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = [a, c]\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_ordinal_is_leD[dest]:
  assumes "a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b"
  shows "[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
proof(intro cat_ordinal_is_arrI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. a \<in>\<^sub>\<circ> A
 2. b \<in>\<^sub>\<circ> A
 3. a \<subseteq>\<^sub>\<circ> b
 4. [a, b]\<^sub>\<circ> = [a, b]\<^sub>\<circ>
[PROOF STEP]
from is_leD[OF assms]
[PROOF STATE]
proof (chain)
picking this:
Hom (cat_ordinal A) a b \<noteq> []\<^sub>\<circ>
[PROOF STEP]
obtain f where "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
using this:
Hom (cat_ordinal A) a b \<noteq> []\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>f. f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (4 subgoals):
 1. a \<in>\<^sub>\<circ> A
 2. b \<in>\<^sub>\<circ> A
 3. a \<subseteq>\<^sub>\<circ> b
 4. [a, b]\<^sub>\<circ> = [a, b]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
show "a \<in>\<^sub>\<circ> A" "b \<in>\<^sub>\<circ> A" "a \<subseteq>\<^sub>\<circ> b"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A &&& a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

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


[STATEMENT]
lemma cat_ordinal_is_leE[elim]:
  assumes "a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b"
  obtains "[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. ([a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma cat_ordinal_is_le_iff:
  "a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<longleftrightarrow> [a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b) = [a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
using cat_ordinal_is_leD cat_ordinal_is_leE
[PROOF STATE]
proof (prove)
using this:
?a \<le>\<^sub>O\<^bsub>cat_ordinal ?A\<^esub> ?b \<Longrightarrow> [?a, ?b]\<^sub>\<circ> : ?a \<mapsto>\<^bsub>cat_ordinal ?A\<^esub> ?b
\<lbrakk>?a \<le>\<^sub>O\<^bsub>cat_ordinal ?A\<^esub> ?b; [?a, ?b]\<^sub>\<circ> : ?a \<mapsto>\<^bsub>cat_ordinal ?A\<^esub> ?b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b) = [a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
by (metis HomI is_le_def vempty_nin)


[STATEMENT]
lemma (in \<Z>) cat_linear_order_cat_ordinal[cat_ordinal_cs_intros]:
  assumes "Ord A" and "A \<subseteq>\<^sub>\<circ> \<alpha>"
  shows "cat_linear_order \<alpha> (cat_ordinal A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_linear_order \<alpha> (cat_ordinal A)
[PROOF STEP]
proof(intro cat_linear_orderI cat_partial_orderI cat_preorderI categoryI')
[PROOF STATE]
proof (state)
goal (23 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (cat_ordinal A)
 3. vcard (cat_ordinal A) = 6\<^sub>\<nat>
 4. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 5. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 6. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 7. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 9. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
A total of 23 subgoals...
[PROOF STEP]
show "vfsequence (cat_ordinal A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (cat_ordinal A)
[PROOF STEP]
unfolding cat_ordinal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [A, ordinal_arrs A, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfsequence (cat_ordinal A)

goal (22 subgoals):
 1. \<Z> \<alpha>
 2. vcard (cat_ordinal A) = 6\<^sub>\<nat>
 3. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 5. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 6. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 10. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
A total of 22 subgoals...
[PROOF STEP]
show "vcard (cat_ordinal A) = 6\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (cat_ordinal A) = 6\<^sub>\<nat>
[PROOF STEP]
unfolding cat_ordinal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [A, ordinal_arrs A, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>[]\<^sub>\<circ>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>ordinal_arrs A. f\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>gf\<in>\<^sub>\<circ>ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}. [gf\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<lambda>x\<in>\<^sub>\<circ>A. [x, x]\<^sub>\<circ>]\<^sub>\<circ> = 6\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (cat_ordinal A) = 6\<^sub>\<nat>

goal (21 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 9. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
 10. \<And>gf. (gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Comp\<rparr>)) = (\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b)
A total of 21 subgoals...
[PROOF STEP]
show "\<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
[PROOF STEP]
by (rule cat_ordinal_Dom_vrange)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>

goal (20 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>gf. (gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Comp\<rparr>)) = (\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b)
 10. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
A total of 20 subgoals...
[PROOF STEP]
show "\<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
[PROOF STEP]
by (rule cat_ordinal_Cod_vrange)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>

goal (19 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<And>gf. (gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Comp\<rparr>)) = (\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b)
 9. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 10. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c; f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
A total of 19 subgoals...
[PROOF STEP]
show "(gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Comp\<rparr>)) \<longleftrightarrow>
    (
      \<exists>g f b c a.
        gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
    )"
    for gf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Comp\<rparr>)) = (\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b)
[PROOF STEP]
unfolding cat_ordinal_Comp_vdomain
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}) = (\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c} \<Longrightarrow> \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
 2. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
assume "gf \<in>\<^sub>\<circ> ordinal_composable A"
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}

goal (2 subgoals):
 1. gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c} \<Longrightarrow> \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
 2. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
obtain a b c
      where gf_def: "gf = [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ>"
        and a: "a \<in>\<^sub>\<circ> A"
        and b: "b \<in>\<^sub>\<circ> A"
        and c: "c \<in>\<^sub>\<circ> A"
        and ab: "a \<le> b"
        and bc: "b \<le> c"
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}

goal (1 subgoal):
 1. (\<And>b c a. \<lbrakk>gf = [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ>; a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> A; c \<in>\<^sub>\<circ> A; a \<subseteq>\<^sub>\<circ> b; b \<subseteq>\<^sub>\<circ> c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
gf = [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
b \<subseteq>\<^sub>\<circ> c

goal (2 subgoals):
 1. gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c} \<Longrightarrow> \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
 2. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
from a b c ab bc
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
b \<subseteq>\<^sub>\<circ> c
[PROOF STEP]
show
      "\<exists>g f b c a.
        gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
b \<subseteq>\<^sub>\<circ> c

goal (1 subgoal):
 1. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
unfolding gf_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
b \<subseteq>\<^sub>\<circ> c

goal (1 subgoal):
 1. \<exists>g f ba ca aa. [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> = [g, f]\<^sub>\<circ> \<and> g : ba \<mapsto>\<^bsub>cat_ordinal A\<^esub> ca \<and> f : aa \<mapsto>\<^bsub>cat_ordinal A\<^esub> ba
[PROOF STEP]
by (intro exI conjI)
        (
          cs_concl cs_shallow
            cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
        )+
[PROOF STATE]
proof (state)
this:
\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
assume
      "\<exists>g f b c a.
        gf = [g, f]\<^sub>\<circ> \<and>
        g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and>
        f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (state)
this:
\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
obtain g f b c a
      where gf_def: "gf = [g, f]\<^sub>\<circ>"
        and g: "g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c"
        and f: "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
using this:
\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. (\<And>g f b c a. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c; f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
gf = [g, f]\<^sub>\<circ>
g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
note g = cat_ordinal_is_arrD[OF g]
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
g = [b, c]\<^sub>\<circ>

goal (1 subgoal):
 1. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
note f = cat_ordinal_is_arrD[OF f]
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. \<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
from g(1-3) f(1-3)
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
show "gf \<in>\<^sub>\<circ> ordinal_composable A"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
unfolding gf_def g(4) f(4)
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. [[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
        )
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> ZFC_in_HOL.set {[[b, c]\<^sub>\<circ>, [a, b]\<^sub>\<circ>]\<^sub>\<circ> |a b c. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> c \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b \<and> b \<subseteq>\<^sub>\<circ> c}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Comp\<rparr>)) = (\<exists>g f b c a. ?gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<and> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b)

goal (18 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c; f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
 10. \<And>c d h b g a f. \<lbrakk>h : c \<mapsto>\<^bsub>cat_ordinal A\<^esub> d; g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c; f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b\<rbrakk> \<Longrightarrow> h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)
A total of 18 subgoals...
[PROOF STEP]
show [cat_ordinal_cs_intros]: "g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c"
    if "g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c" and "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b" for b c g a f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
[PROOF STEP]
note g = cat_ordinal_is_arrD[OF that(1)]
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
g = [b, c]\<^sub>\<circ>

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
[PROOF STEP]
note f = cat_ordinal_is_arrD[OF that(2)]
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
[PROOF STEP]
proof(intro cat_ordinal_is_arrI g(1,2) f(1,2), unfold g(4) f(4))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<subseteq>\<^sub>\<circ> c
 2. [b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ> = [a, c]\<^sub>\<circ>
[PROOF STEP]
from g(3) f(3)
[PROOF STATE]
proof (chain)
picking this:
b \<subseteq>\<^sub>\<circ> c
a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
show "a \<subseteq>\<^sub>\<circ> c"
[PROOF STATE]
proof (prove)
using this:
b \<subseteq>\<^sub>\<circ> c
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. a \<subseteq>\<^sub>\<circ> c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<subseteq>\<^sub>\<circ> c

goal (1 subgoal):
 1. [b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ> = [a, c]\<^sub>\<circ>
[PROOF STEP]
from g(1,2,3) f(1,2,3)
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
show " [b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ> = [a, c]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. [b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ> = [a, c]\<^sub>\<circ>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
          )
[PROOF STATE]
proof (state)
this:
[b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ> = [a, c]\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?g : ?b \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?c; ?f : ?a \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?b\<rbrakk> \<Longrightarrow> ?g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> ?f : ?a \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?c

goal (17 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>c d h b g a f. \<lbrakk>h : c \<mapsto>\<^bsub>cat_ordinal A\<^esub> d; g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c; f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b\<rbrakk> \<Longrightarrow> h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)
 10. \<And>a. a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr> \<Longrightarrow> cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a
A total of 17 subgoals...
[PROOF STEP]
show
    "h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f =
      h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)"
    if "h : c \<mapsto>\<^bsub>cat_ordinal A\<^esub> d"
      and "g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c"
      and "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
    for c d h b g a f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)
[PROOF STEP]
note h = cat_ordinal_is_arrD[OF that(1)]
[PROOF STATE]
proof (state)
this:
c \<in>\<^sub>\<circ> A
d \<in>\<^sub>\<circ> A
c \<subseteq>\<^sub>\<circ> d
h = [c, d]\<^sub>\<circ>

goal (1 subgoal):
 1. h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)
[PROOF STEP]
note g = cat_ordinal_is_arrD[OF that(2)]
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
g = [b, c]\<^sub>\<circ>

goal (1 subgoal):
 1. h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)
[PROOF STEP]
note f = cat_ordinal_is_arrD[OF that(3)]
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)
[PROOF STEP]
from that(1-3) h(1-3) g(1-4) f(1-3)
[PROOF STATE]
proof (chain)
picking this:
h : c \<mapsto>\<^bsub>cat_ordinal A\<^esub> d
g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
c \<in>\<^sub>\<circ> A
d \<in>\<^sub>\<circ> A
c \<subseteq>\<^sub>\<circ> d
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
g = [b, c]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h : c \<mapsto>\<^bsub>cat_ordinal A\<^esub> d
g : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
c \<in>\<^sub>\<circ> A
d \<in>\<^sub>\<circ> A
c \<subseteq>\<^sub>\<circ> d
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
g = [b, c]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)
[PROOF STEP]
unfolding h(4) g(4) f(4)
[PROOF STATE]
proof (prove)
using this:
[c, d]\<^sub>\<circ> : c \<mapsto>\<^bsub>cat_ordinal A\<^esub> d
[b, c]\<^sub>\<circ> : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
c \<in>\<^sub>\<circ> A
d \<in>\<^sub>\<circ> A
c \<subseteq>\<^sub>\<circ> d
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
[b, c]\<^sub>\<circ> = [b, c]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. [c, d]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ> = [c, d]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> ([b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ>)
[PROOF STEP]
(*slow*)
[PROOF STATE]
proof (prove)
using this:
[c, d]\<^sub>\<circ> : c \<mapsto>\<^bsub>cat_ordinal A\<^esub> d
[b, c]\<^sub>\<circ> : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c
[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
c \<in>\<^sub>\<circ> A
d \<in>\<^sub>\<circ> A
c \<subseteq>\<^sub>\<circ> d
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
[b, c]\<^sub>\<circ> = [b, c]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. [c, d]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ> = [c, d]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> ([b, c]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> [a, b]\<^sub>\<circ>)
[PROOF STEP]
by (cs_concl cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros)
[PROOF STATE]
proof (state)
this:
h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?h : ?c \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?d; ?g : ?b \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?c; ?f : ?a \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?b\<rbrakk> \<Longrightarrow> ?h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> ?g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> ?f = ?h \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> (?g \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> ?f)

goal (16 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>a. a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr> \<Longrightarrow> cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a
 10. \<And>a b f. f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = f
A total of 16 subgoals...
[PROOF STEP]
show "cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a"
    if "a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
[PROOF STEP]
have "a \<in>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
[PROOF STEP]
show "cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_ordinal_cs_simps
            cs_intro: cat_ordinal_cs_intros V_cs_intros
        )
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr> \<Longrightarrow> cat_ordinal A\<lparr>CId\<rparr>\<lparr>?a\<rparr> : ?a \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?a

goal (15 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>a b f. f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b \<Longrightarrow> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = f
 10. \<And>b c f. f : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
A total of 15 subgoals...
[PROOF STEP]
show "cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = f"
    if "f : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b" for a b f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = f
[PROOF STEP]
note f = cat_ordinal_is_arrD[OF that]
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
f = [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = f
[PROOF STEP]
from f(1-3)
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = f
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_ordinal_cs_simps f(4)
            cs_intro: cat_ordinal_cs_intros V_cs_intros
        )
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> f = f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?b \<Longrightarrow> cat_ordinal A\<lparr>CId\<rparr>\<lparr>?b\<rparr> \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> ?f = ?f

goal (14 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>b c f. f : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
 10. cat_ordinal A\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
A total of 14 subgoals...
[PROOF STEP]
show "f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> = f"
    if "f : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c" for b c f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
note f = cat_ordinal_is_arrD[OF that]
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
f = [b, c]\<^sub>\<circ>

goal (1 subgoal):
 1. f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
from f(1-3)
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c

goal (1 subgoal):
 1. f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_ordinal_cs_simps f(4)
            cs_intro: cat_ordinal_cs_intros V_cs_intros
        )
[PROOF STATE]
proof (state)
this:
f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>b\<rparr> = f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f : ?b \<mapsto>\<^bsub>cat_ordinal A\<^esub> ?c \<Longrightarrow> ?f \<circ>\<^sub>A\<^bsub>cat_ordinal A\<^esub> cat_ordinal A\<lparr>CId\<rparr>\<lparr>?b\<rparr> = ?f

goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. cat_ordinal A\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 10. \<And>Aa B. \<lbrakk>Aa \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; Aa \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>Aa. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_ordinal A) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> Aa) \<in>\<^sub>\<circ> Vset \<alpha>
A total of 13 subgoals...
[PROOF STEP]
from assms Ord_\<alpha>
[PROOF STATE]
proof (chain)
picking this:
Ord A
A \<subseteq>\<^sub>\<circ> \<alpha>
Ord \<alpha>
[PROOF STEP]
show "cat_ordinal A\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Ord A
A \<subseteq>\<^sub>\<circ> \<alpha>
Ord \<alpha>

goal (1 subgoal):
 1. cat_ordinal A\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
using this:
Ord A
A \<subseteq>\<^sub>\<circ> \<alpha>
Ord \<alpha>

goal (1 subgoal):
 1. A \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>Aa B. \<lbrakk>Aa \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; Aa \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>Aa. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_ordinal A) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> Aa) \<in>\<^sub>\<circ> Vset \<alpha>
 10. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
A total of 12 subgoals...
[PROOF STEP]
show "(\<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ>c\<in>\<^sub>\<circ>C. Hom (cat_ordinal A) b c) \<in>\<^sub>\<circ> Vset \<alpha>"
    if "B \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>"
      and "C \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>"
      and "B \<in>\<^sub>\<circ> Vset \<alpha>"
      and "C \<in>\<^sub>\<circ> Vset \<alpha>"
    for B C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ>c\<in>\<^sub>\<circ>C. Hom (cat_ordinal A) b c) \<subseteq>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<subseteq>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
[PROOF STEP]
proof(rule vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<Longrightarrow> x \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<Longrightarrow> x \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
[PROOF STEP]
assume "f \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ>c\<in>\<^sub>\<circ>C. Hom (cat_ordinal A) b c)"
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<Longrightarrow> x \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B)
[PROOF STEP]
obtain b c
        where b: "b \<in>\<^sub>\<circ> B" and c: "c \<in>\<^sub>\<circ> C" and f: "f : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B)

goal (1 subgoal):
 1. (\<And>b c. \<lbrakk>b \<in>\<^sub>\<circ> B; c \<in>\<^sub>\<circ> C; f : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> B
c \<in>\<^sub>\<circ> C
f : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> c

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<Longrightarrow> x \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
[PROOF STEP]
note f = cat_ordinal_is_arrD[OF f]
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> A
c \<in>\<^sub>\<circ> A
b \<subseteq>\<^sub>\<circ> c
f = [b, c]\<^sub>\<circ>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<Longrightarrow> x \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
[PROOF STEP]
from b c
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> B
c \<in>\<^sub>\<circ> C
[PROOF STEP]
show "f \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> B
c \<in>\<^sub>\<circ> C

goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
[PROOF STEP]
unfolding f(4)
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> B
c \<in>\<^sub>\<circ> C

goal (1 subgoal):
 1. [b, c]\<^sub>\<circ> \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<subseteq>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<subseteq>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from that(3,4)
[PROOF STATE]
proof (chain)
picking this:
B \<in>\<^sub>\<circ> Vset \<alpha>
C \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "B \<times>\<^sub>\<bullet> C \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
B \<in>\<^sub>\<circ> Vset \<alpha>
C \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. B \<times>\<^sub>\<bullet> C \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto intro: Limit_ftimes_in_VsetI)
[PROOF STATE]
proof (state)
this:
B \<times>\<^sub>\<bullet> C \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<subseteq>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
B \<times>\<^sub>\<bullet> C \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>B. \<Union>\<^sub>\<circ> (VLambda C (Hom (cat_ordinal A) a) `\<^sub>\<circ> C)) `\<^sub>\<circ> B) \<subseteq>\<^sub>\<circ> B \<times>\<^sub>\<bullet> C
B \<times>\<^sub>\<bullet> C \<in>\<^sub>\<circ> Vset \<alpha>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?B \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; ?C \<subseteq>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; ?B \<in>\<^sub>\<circ> Vset \<alpha>; ?C \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>?B. \<Union>\<^sub>\<circ> (VLambda ?C (Hom (cat_ordinal A) a) `\<^sub>\<circ> ?C)) `\<^sub>\<circ> ?B) \<in>\<^sub>\<circ> Vset \<alpha>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
 10. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b; b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a\<rbrakk> \<Longrightarrow> a = b
A total of 11 subgoals...
[PROOF STEP]
show "(\<exists>f. Hom (cat_ordinal A) a b = set {f}) \<or> Hom (cat_ordinal A) a b = 0"
    if "a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>" and "b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
[PROOF STEP]
have a: "a \<in>\<^sub>\<circ> A" and b: "b \<in>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
[PROOF STEP]
consider \<open>a \<le> b\<close> | \<open>\<not>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A

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

goal (1 subgoal):
 1. (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> ?thesis; \<not> a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> ?thesis; \<not> a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
 2. \<not> a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
a \<subseteq>\<^sub>\<circ> b

goal (2 subgoals):
 1. a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
 2. \<not> a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
with a b
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b
[PROOF STEP]
have "[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
a \<subseteq>\<^sub>\<circ> b

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
by (auto intro: cat_ordinal_is_arrI)
[PROOF STATE]
proof (state)
this:
[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (2 subgoals):
 1. a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
 2. \<not> a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b

goal (1 subgoal):
 1. (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
by (simp add: cat_ordinal_Hom_ne)
[PROOF STATE]
proof (state)
this:
(\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>

goal (1 subgoal):
 1. \<not> a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>
[PROOF STEP]
qed (simp add: cat_ordinal_Hom_empty)
[PROOF STATE]
proof (state)
this:
(\<exists>f. Hom (cat_ordinal A) a b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) a b = []\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<exists>f. Hom (cat_ordinal A) ?a ?b = ZFC_in_HOL.set {f}) \<or> Hom (cat_ordinal A) ?a ?b = []\<^sub>\<circ>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b; b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a\<rbrakk> \<Longrightarrow> a = b
 10. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
show "a = b"
    if "a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>"
      and "b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>"
      and "a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b"
      and "b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a"
    for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
using
      that(3,4)[unfolded cat_ordinal_is_le_iff cat_ordinal_components]
      cat_ordinal_is_arr_is_unique
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> : a \<mapsto>\<^bsub>cat_ordinal A\<^esub> b
[b, a]\<^sub>\<circ> : b \<mapsto>\<^bsub>cat_ordinal A\<^esub> a
\<lbrakk>?f : ?a \<mapsto>\<^bsub>cat_ordinal ?A\<^esub> ?b; ?g : ?a \<mapsto>\<^bsub>cat_ordinal ?A\<^esub> ?b\<rbrakk> \<Longrightarrow> ?f = ?g

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; ?a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> ?b; ?b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> ?a\<rbrakk> \<Longrightarrow> ?a = ?b

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
 9. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
show "a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a"
    if "a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>" and "b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
from that[unfolded cat_ordinal_components]
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
[PROOF STEP]
have a: "a \<in>\<^sub>\<circ> A" and b: "b \<in>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> A &&& b \<in>\<^sub>\<circ> A
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Ord A
A \<subseteq>\<^sub>\<circ> \<alpha>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A
[PROOF STEP]
have "Ord a" "Ord b"
[PROOF STATE]
proof (prove)
using this:
Ord A
A \<subseteq>\<^sub>\<circ> \<alpha>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. Ord a &&& Ord b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ord a
Ord b

goal (1 subgoal):
 1. a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ord a
Ord b
[PROOF STEP]
consider \<open>a \<le> b\<close> | \<open>b \<le> a\<close>
[PROOF STATE]
proof (prove)
using this:
Ord a
Ord b

goal (1 subgoal):
 1. \<lbrakk>a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> thesis; b \<subseteq>\<^sub>\<circ> a \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (meson Ord_linear_le)
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> ?thesis; b \<subseteq>\<^sub>\<circ> a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> ?thesis; b \<subseteq>\<^sub>\<circ> a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<subseteq>\<^sub>\<circ> b \<Longrightarrow> ?thesis; b \<subseteq>\<^sub>\<circ> a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a
[PROOF STEP]
by cases (auto simp: a b cat_ordinal_is_le_iff intro: cat_ordinal_is_arrI)
[PROOF STATE]
proof (state)
this:
a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> b \<or> b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> cat_ordinal A\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> ?a \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> ?b \<or> ?b \<le>\<^sub>O\<^bsub>cat_ordinal A\<^esub> ?a

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_ordinal A\<lparr>Dom\<rparr>)
 3. vsv (cat_ordinal A\<lparr>Cod\<rparr>)
 4. vsv (cat_ordinal A\<lparr>Comp\<rparr>)
 5. vsv (cat_ordinal A\<lparr>CId\<rparr>)
 6. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Dom\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 7. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>Cod\<rparr>) = cat_ordinal A\<lparr>Arr\<rparr>
 8. \<D>\<^sub>\<circ> (cat_ordinal A\<lparr>CId\<rparr>) = cat_ordinal A\<lparr>Obj\<rparr>
[PROOF STEP]
qed (auto intro: cat_ordinal_cs_intros simp: cat_ordinal_cs_simps)