# Theory CZH_ECAT_Ordinal

```(* Copyright 2020 (C) Mihails Milehins *)

section‹Ordinal numbers›
theory CZH_ECAT_Ordinal
imports CZH_ECAT_Small_Order
begin

subsection‹Background›

text‹
The content of this section is based on the treatment of the ordinal numbers
from the perspective of category theory as exposed, for example,
in Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.
›

named_theorems cat_ordinal_cs_simps
named_theorems cat_ordinal_cs_intros

subsection‹Arrows associated with an ordinal number›

definition ordinal_arrs :: "V ⇒ V"
where "ordinal_arrs A ≡ set {[a, b]⇩∘ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ a ≤ b}"

lemma small_ordinal_arrs[simp]:
"small {[a, b]⇩∘ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ a ≤ b}"
by (rule down[where x=‹A ×⇩∙ A›]) auto

text‹Rules.›

lemma ordinal_arrsI[cat_ordinal_cs_intros]:
assumes "x = [a, b]⇩∘" and "a ∈⇩∘ A" and "b ∈⇩∘ A" and "a ≤ b"
shows "x ∈⇩∘ ordinal_arrs A"
using assms unfolding ordinal_arrs_def by auto

lemma ordinal_arrsD[dest]:
assumes "[a, b]⇩∘ ∈⇩∘ ordinal_arrs A"
shows "a ∈⇩∘ A" and "b ∈⇩∘ A" and "a ≤ b"
using assms unfolding ordinal_arrs_def by auto

lemma ordinal_arrsE[elim]:
assumes "x ∈⇩∘ ordinal_arrs A"
obtains a b where "a ∈⇩∘ A" and "b ∈⇩∘ A" and "a ≤ b" and "x = [a, b]⇩∘"
using assms unfolding ordinal_arrs_def by clarsimp

subsection‹Composable arrows›

abbreviation ordinal_composable :: "V ⇒ V"
where "ordinal_composable A ≡ set
{
[[b, c]⇩∘, [a, b]⇩∘]⇩∘ | a b c.
a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ c ∈⇩∘ A ∧ a ≤ b ∧ b ≤ c
}"

lemma small_ordinal_composable[simp]:
"small
{
[[b, c]⇩∘, [a, b]⇩∘]⇩∘ | a b c.
a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ c ∈⇩∘ A ∧ a ≤ b ∧ b ≤ c
}"
by (rule down[where x=‹(A ×⇩∙ A) ×⇩∙ (A ×⇩∙ A)›]) auto

text‹Rules.›

lemma ordinal_composableI[cat_ordinal_cs_intros]:
assumes "x = [[b, c]⇩∘, [a, b]⇩∘]⇩∘"
and "a ∈⇩∘ A"
and "b ∈⇩∘ A"
and "c ∈⇩∘ A"
and "a ≤ b"
and "b ≤ c"
shows "x ∈⇩∘ ordinal_composable A"
using assms by auto

lemma ordinal_composableD[dest]:
assumes "[[b, c]⇩∘, [a, b]⇩∘]⇩∘ ∈⇩∘ ordinal_composable A"
shows "a ∈⇩∘ A" and "b ∈⇩∘ A" and "c ∈⇩∘ A" and "a ≤ b" and "b ≤ c"
using assms by auto

lemma ordinal_composableE[elim]:
assumes "x ∈⇩∘ ordinal_composable A"
obtains a b c
where "x = [[b, c]⇩∘, [a, b]⇩∘]⇩∘"
and "a ∈⇩∘ A"
and "b ∈⇩∘ A"
and "c ∈⇩∘ A"
and "a ≤ b"
and "b ≤ c"
using assms by clarsimp

subsection‹Ordinal number as a category›

subsubsection‹Definition and elementary properties›

definition cat_ordinal :: "V ⇒ V"
where "cat_ordinal A =
[
A,
ordinal_arrs A,
(λf∈⇩∘ordinal_arrs A. f⦇0⦈),
(λf∈⇩∘ordinal_arrs A. f⦇1⇩ℕ⦈),
(λgf∈⇩∘ordinal_composable A. [gf⦇1⇩ℕ⦈⦇0⦈, gf⦇0⦈⦇1⇩ℕ⦈]⇩∘),
(λx∈⇩∘A. [x, x]⇩∘)
]⇩∘"

text‹Components.›

lemma cat_ordinal_components:
shows [cat_ordinal_cs_simps]: "cat_ordinal A⦇Obj⦈ = A"
and [cat_ordinal_cs_simps]: "cat_ordinal A⦇Arr⦈ = ordinal_arrs A"
and "cat_ordinal A⦇Dom⦈ = (λf∈⇩∘ordinal_arrs A. f⦇0⦈)"
and "cat_ordinal A⦇Cod⦈ = (λf∈⇩∘ordinal_arrs A. f⦇1⇩ℕ⦈)"
and "cat_ordinal A⦇Comp⦈ =
(λgf∈⇩∘ordinal_composable A. [gf⦇1⇩ℕ⦈⦇0⦈, gf⦇0⦈⦇1⇩ℕ⦈]⇩∘)"
and "cat_ordinal A⦇CId⦈ = (λx∈⇩∘A. [x, x]⇩∘)"
unfolding cat_ordinal_def dg_field_simps by (simp_all add: nat_omega_simps)

subsubsection‹Domain›

mk_VLambda cat_ordinal_components(3)
|vsv cat_ordinal_Dom_vsv[cat_ordinal_cs_intros]|
|vdomain
cat_ordinal_Dom_vdomain[
folded cat_ordinal_components, cat_ordinal_cs_simps
]
|

lemma cat_ordinal_Dom_app[cat_ordinal_cs_simps]:
assumes "x ∈⇩∘ cat_ordinal A⦇Arr⦈" and "x = [a, b]⇩∘"
shows "cat_ordinal A⦇Dom⦈⦇x⦈ = a"
using assms(1) unfolding assms(2) cat_ordinal_components by auto

lemma cat_ordinal_Dom_vrange: "ℛ⇩∘ (cat_ordinal A⦇Dom⦈) ⊆⇩∘ cat_ordinal A⦇Obj⦈"
unfolding cat_ordinal_components
by (intro vrange_VLambda_vsubset, elim ordinal_arrsE) simp

subsubsection‹Codomain›

mk_VLambda cat_ordinal_components(4)
|vsv cat_ordinal_Cod_vsv[cat_ordinal_cs_intros]|
|vdomain
cat_ordinal_Cod_vdomain[
folded cat_ordinal_components, cat_ordinal_cs_simps
]
|

lemma cat_ordinal_Cod_app[cat_ordinal_cs_simps]:
assumes "x ∈⇩∘ cat_ordinal A⦇Arr⦈" and "x = [a, b]⇩∘"
shows "cat_ordinal A⦇Cod⦈⦇x⦈ = b"
using assms(1)
unfolding assms(2) cat_ordinal_components
by (auto simp: nat_omega_simps)

lemma cat_ordinal_Cod_vrange: "ℛ⇩∘ (cat_ordinal A⦇Cod⦈) ⊆⇩∘ cat_ordinal A⦇Obj⦈"
unfolding cat_ordinal_components
by (intro vrange_VLambda_vsubset, elim ordinal_arrsE)

subsubsection‹Arrow with a domain and a codomain›

text‹Rules.›

lemma cat_ordinal_is_arrI[cat_ordinal_cs_intros]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A" and "a ≤ b" and "f = [a, b]⇩∘"
shows "f : a ↦⇘cat_ordinal A⇙ b"
proof(intro is_arrI, unfold cat_ordinal_components(2))
from assms show "f ∈⇩∘ ordinal_arrs A" by (intro ordinal_arrsI)
then show "cat_ordinal A⦇Dom⦈⦇f⦈ = a" "cat_ordinal A⦇Cod⦈⦇f⦈ = b"
by (cs_concl cs_simp: cat_ordinal_cs_simps assms(4))+
qed

lemma cat_ordinal_is_arrD[dest]:
assumes "f : a ↦⇘cat_ordinal A⇙ b"
shows "a ∈⇩∘ A" and "b ∈⇩∘ A" and "a ≤ b" and "f = [a, b]⇩∘"
proof-
note f = is_arrD[OF assms, unfolded cat_ordinal_components(2)]
from f(1) obtain a' b'
where a': "a' ∈⇩∘ A"
and b': "b' ∈⇩∘ A"
and a'b': "a' ≤ b'"
and f_def: "f = [a', b']⇩∘"
unfolding ordinal_arrs_def by clarsimp
from f(2) a' b' a'b' have a'_def: "a' = a"
by
(
cs_prems cs_shallow
cs_simp: cat_ordinal_cs_simps f_def cs_intro: cat_ordinal_cs_intros
)
from f(3) a' b' a'b' have b'_def: "b' = b"
by
(
cs_prems cs_shallow
cs_simp: cat_ordinal_cs_simps f_def cs_intro: cat_ordinal_cs_intros
)
from a' b' a'b' f_def show "a ∈⇩∘ A" and "b ∈⇩∘ A" and "a ≤ b" and "f = [a, b]⇩∘"
unfolding a'_def b'_def by auto
qed

lemma cat_ordinal_is_arrE[elim]:
assumes "f : a ↦⇘cat_ordinal A⇙ b"
obtains "a ∈⇩∘ A" and "b ∈⇩∘ A" and "a ≤ b" and "f = [a, b]⇩∘"
using assms by auto

text‹Elementary properties.›

lemma cat_ordinal_is_arr_not:
assumes "¬a ≤ b"
shows "¬f : a ↦⇘cat_ordinal A⇙ b"
proof(rule ccontr, unfold not_not)
assume "f : a ↦⇘cat_ordinal A⇙ b"
with cat_ordinal_is_arrD(3)[OF this] assms show False by simp
qed

lemma cat_ordinal_is_arr_is_unique:
assumes "f : a ↦⇘cat_ordinal A⇙ b" and "g : a ↦⇘cat_ordinal A⇙ b"
shows "f = g"
by
(
cat_ordinal_is_arrD(4)[OF assms(1)]
cat_ordinal_is_arrD(4)[OF assms(2)]
)

lemma cat_ordinal_Hom_ne:
assumes "f : a ↦⇘cat_ordinal A⇙ b"
shows "Hom (cat_ordinal A) a b = set {f}"
using assms cat_ordinal_is_arr_is_unique
by (intro vsubset_antisym vsubsetI) auto

lemma cat_ordinal_Hom_empty:
assumes "¬a ≤ b"
shows "Hom (cat_ordinal A) a b = 0"
using assms by (intro vsubset_antisym vsubsetI) auto

lemma cat_ordinal_inj:
assumes "cat_ordinal m = cat_ordinal n"
shows "m = n"
by (metis assms cat_ordinal_components(1))

subsubsection‹Composition›

mk_VLambda cat_ordinal_components(5)
|vsv cat_ordinal_Comp_vsv[cat_ordinal_cs_intros]|
|vdomain cat_ordinal_Comp_vdomain[folded cat_ordinal_components, cat_cs_simps]|

lemma cat_ordinal_Comp_app[cat_ordinal_cs_simps]:
assumes "g : b ↦⇘cat_ordinal A⇙ c" and "f : a ↦⇘cat_ordinal A⇙ b"
shows "g ∘⇩A⇘cat_ordinal A⇙ f = [a, c]⇩∘"
proof-
from assms(2) have a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ A"
and ab: "a ≤ b"
and f_def: "f = [a, b]⇩∘"
by auto
from assms(1) have c: "c ∈⇩∘ A" and bc: "b ≤ c" and g_def: "g = [b, c]⇩∘"
by auto
from a b c ab bc have "[g, f]⇩∘ ∈⇩∘ ordinal_composable A"
by (cs_concl cs_shallow cs_simp: g_def f_def cs_intro: cat_ordinal_cs_intros)
then show "g ∘⇩A⇘cat_ordinal A⇙ f = [a, c]⇩∘"
unfolding cat_ordinal_components by (simp add: g_def f_def nat_omega_simps)
qed

subsubsection‹Identity›

mk_VLambda cat_ordinal_components(6)
|vsv cat_ordinal_CId_vsv[cat_ordinal_cs_intros]|
|vdomain cat_ordinal_CId_vdomain[cat_ordinal_cs_simps]|
|app cat_ordinal_CId_app[cat_ordinal_cs_simps]|

subsubsection‹Order relation›

lemma cat_ordinal_is_leD[dest]:
assumes "a ≤⇩O⇘cat_ordinal A⇙ b"
shows "[a, b]⇩∘ : a ↦⇘cat_ordinal A⇙ b"
proof(intro cat_ordinal_is_arrI)
from is_leD[OF assms] obtain f where "f : a ↦⇘cat_ordinal A⇙ b" by fastforce
then show "a ∈⇩∘ A" "b ∈⇩∘ A" "a ⊆⇩∘ b" by auto
qed simp

lemma cat_ordinal_is_leE[elim]:
assumes "a ≤⇩O⇘cat_ordinal A⇙ b"
obtains "[a, b]⇩∘ : a ↦⇘cat_ordinal A⇙ b"
using assms by auto

lemma cat_ordinal_is_le_iff:
"a ≤⇩O⇘cat_ordinal A⇙ b ⟷ [a, b]⇩∘ : a ↦⇘cat_ordinal A⇙ b"
using cat_ordinal_is_leD cat_ordinal_is_leE
by (metis HomI is_le_def vempty_nin)

subsubsection‹Every ordinal number is a category›

lemma (in 𝒵) cat_linear_order_cat_ordinal[cat_ordinal_cs_intros]:
assumes "Ord A" and "A ⊆⇩∘ α"
shows "cat_linear_order α (cat_ordinal A)"
proof(intro cat_linear_orderI cat_partial_orderI cat_preorderI categoryI')
show "vfsequence (cat_ordinal A)" unfolding cat_ordinal_def by auto
show "vcard (cat_ordinal A) = 6⇩ℕ"
unfolding cat_ordinal_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (cat_ordinal A⦇Dom⦈) ⊆⇩∘ cat_ordinal A⦇Obj⦈"
by (rule cat_ordinal_Dom_vrange)
show "ℛ⇩∘ (cat_ordinal A⦇Cod⦈) ⊆⇩∘ cat_ordinal A⦇Obj⦈"
by (rule cat_ordinal_Cod_vrange)
show "(gf ∈⇩∘ 𝒟⇩∘ (cat_ordinal A⦇Comp⦈)) ⟷
(
∃g f b c a.
gf = [g, f]⇩∘ ∧ g : b ↦⇘cat_ordinal A⇙ c ∧ f : a ↦⇘cat_ordinal A⇙ b
)"
for gf
unfolding cat_ordinal_Comp_vdomain
proof
assume "gf ∈⇩∘ ordinal_composable A"
then obtain a b c
where gf_def: "gf = [[b, c]⇩∘, [a, b]⇩∘]⇩∘"
and a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ A"
and c: "c ∈⇩∘ A"
and ab: "a ≤ b"
and bc: "b ≤ c"
by clarsimp
from a b c ab bc show
"∃g f b c a.
gf = [g, f]⇩∘ ∧ g : b ↦⇘cat_ordinal A⇙ c ∧ f : a ↦⇘cat_ordinal A⇙ b"
unfolding gf_def
by (intro exI conjI)
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
)+
next
assume
"∃g f b c a.
gf = [g, f]⇩∘ ∧
g : b ↦⇘cat_ordinal A⇙ c ∧
f : a ↦⇘cat_ordinal A⇙ b"
then obtain g f b c a
where gf_def: "gf = [g, f]⇩∘"
and g: "g : b ↦⇘cat_ordinal A⇙ c"
and f: "f : a ↦⇘cat_ordinal A⇙ b"
by clarsimp
note g = cat_ordinal_is_arrD[OF g]
note f = cat_ordinal_is_arrD[OF f]
from g(1-3) f(1-3) show "gf ∈⇩∘ ordinal_composable A"
unfolding gf_def g(4) f(4)
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
)
qed
show [cat_ordinal_cs_intros]: "g ∘⇩A⇘cat_ordinal A⇙ f : a ↦⇘cat_ordinal A⇙ c"
if "g : b ↦⇘cat_ordinal A⇙ c" and "f : a ↦⇘cat_ordinal A⇙ b" for b c g a f
proof-
note g = cat_ordinal_is_arrD[OF that(1)]
note f = cat_ordinal_is_arrD[OF that(2)]
show ?thesis
proof(intro cat_ordinal_is_arrI g(1,2) f(1,2), unfold g(4) f(4))
from g(3) f(3) show "a ⊆⇩∘ c" by auto
from g(1,2,3) f(1,2,3) show " [b, c]⇩∘ ∘⇩A⇘cat_ordinal A⇙ [a, b]⇩∘ = [a, c]⇩∘"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
)
qed
qed
show
"h ∘⇩A⇘cat_ordinal A⇙ g ∘⇩A⇘cat_ordinal A⇙ f =
h ∘⇩A⇘cat_ordinal A⇙ (g ∘⇩A⇘cat_ordinal A⇙ f)"
if "h : c ↦⇘cat_ordinal A⇙ d"
and "g : b ↦⇘cat_ordinal A⇙ c"
and "f : a ↦⇘cat_ordinal A⇙ b"
for c d h b g a f
proof-
note h = cat_ordinal_is_arrD[OF that(1)]
note g = cat_ordinal_is_arrD[OF that(2)]
note f = cat_ordinal_is_arrD[OF that(3)]
from that(1-3) h(1-3) g(1-4) f(1-3) show ?thesis
unfolding h(4) g(4) f(4) (*slow*)
by (cs_concl cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros)
qed
show "cat_ordinal A⦇CId⦈⦇a⦈ : a ↦⇘cat_ordinal A⇙ a"
if "a ∈⇩∘ cat_ordinal A⦇Obj⦈" for a
proof-
from that have "a ∈⇩∘ A" unfolding cat_ordinal_components by simp
then show "cat_ordinal A⦇CId⦈⦇a⦈ : a ↦⇘cat_ordinal A⇙ a"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps
cs_intro: cat_ordinal_cs_intros V_cs_intros
)
qed
show "cat_ordinal A⦇CId⦈⦇b⦈ ∘⇩A⇘cat_ordinal A⇙ f = f"
if "f : a ↦⇘cat_ordinal A⇙ b" for a b f
proof-
note f = cat_ordinal_is_arrD[OF that]
from f(1-3) show ?thesis
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps f(4)
cs_intro: cat_ordinal_cs_intros V_cs_intros
)
qed
show "f ∘⇩A⇘cat_ordinal A⇙ cat_ordinal A⦇CId⦈⦇b⦈ = f"
if "f : b ↦⇘cat_ordinal A⇙ c" for b c f
proof-
note f = cat_ordinal_is_arrD[OF that]
from f(1-3) show ?thesis
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps f(4)
cs_intro: cat_ordinal_cs_intros V_cs_intros
)
qed
from assms Ord_α show "cat_ordinal A⦇Obj⦈ ⊆⇩∘ Vset α"
unfolding cat_ordinal_components by auto
show "(⋃⇩∘b∈⇩∘B. ⋃⇩∘c∈⇩∘C. Hom (cat_ordinal A) b c) ∈⇩∘ Vset α"
if "B ⊆⇩∘ cat_ordinal A⦇Obj⦈"
and "C ⊆⇩∘ cat_ordinal A⦇Obj⦈"
and "B ∈⇩∘ Vset α"
and "C ∈⇩∘ Vset α"
for B C
proof-
have "(⋃⇩∘b∈⇩∘B. ⋃⇩∘c∈⇩∘C. Hom (cat_ordinal A) b c) ⊆⇩∘ B ×⇩∙ C"
proof(rule vsubsetI)
fix f assume "f ∈⇩∘ (⋃⇩∘b∈⇩∘B. ⋃⇩∘c∈⇩∘C. Hom (cat_ordinal A) b c)"
then obtain b c
where b: "b ∈⇩∘ B" and c: "c ∈⇩∘ C" and f: "f : b ↦⇘cat_ordinal A⇙ c"
by auto
note f = cat_ordinal_is_arrD[OF f]
from b c show "f ∈⇩∘ B ×⇩∙ C"
unfolding f(4) by auto
qed
moreover from that(3,4) have "B ×⇩∙ C ∈⇩∘ Vset α"
by (auto intro: Limit_ftimes_in_VsetI)
ultimately show ?thesis by blast
qed
show "(∃f. Hom (cat_ordinal A) a b = set {f}) ∨ Hom (cat_ordinal A) a b = 0"
if "a ∈⇩∘ cat_ordinal A⦇Obj⦈" and "b ∈⇩∘ cat_ordinal A⦇Obj⦈" for a b
proof-
from that have a: "a ∈⇩∘ A" and b: "b ∈⇩∘ A"
unfolding cat_ordinal_components by simp_all
then consider ‹a ≤ b› | ‹¬a ≤ b› by auto
then show ?thesis
proof cases
case 1
with a b have "[a, b]⇩∘ : a ↦⇘cat_ordinal A⇙ b"
by (auto intro: cat_ordinal_is_arrI)
then show ?thesis by (simp add: cat_ordinal_Hom_ne)
qed (simp add: cat_ordinal_Hom_empty)
qed
show "a = b"
if "a ∈⇩∘ cat_ordinal A⦇Obj⦈"
and "b ∈⇩∘ cat_ordinal A⦇Obj⦈"
and "a ≤⇩O⇘cat_ordinal A⇙ b"
and "b ≤⇩O⇘cat_ordinal A⇙ a"
for a b
using
that(3,4)[unfolded cat_ordinal_is_le_iff cat_ordinal_components]
cat_ordinal_is_arr_is_unique
by auto
show "a ≤⇩O⇘cat_ordinal A⇙ b ∨ b ≤⇩O⇘cat_ordinal A⇙ a"
if "a ∈⇩∘ cat_ordinal A⦇Obj⦈" and "b ∈⇩∘ cat_ordinal A⦇Obj⦈" for a b
proof-
from that[unfolded cat_ordinal_components] have a: "a ∈⇩∘ A" and b: "b ∈⇩∘ A"
by simp_all
with assms have "Ord a" "Ord b" by auto
then consider ‹a ≤ b› | ‹b ≤ a› by (meson Ord_linear_le)
then show "a ≤⇩O⇘cat_ordinal A⇙ b ∨ b ≤⇩O⇘cat_ordinal A⇙ a"
by cases (auto simp: a b cat_ordinal_is_le_iff intro: cat_ordinal_is_arrI)
qed
qed (auto intro: cat_ordinal_cs_intros simp: cat_ordinal_cs_simps)

lemmas [cat_ordinal_cs_intros] = 𝒵.cat_linear_order_cat_ordinal

lemma (in 𝒵) cat_tiny_linear_order_cat_ordinal[cat_ordinal_cs_intros]:
assumes "Ord A" and "A ∈⇩∘ α"
shows "cat_tiny_linear_order α (cat_ordinal A)"
proof(intro cat_tiny_linear_orderI' cat_linear_order_cat_ordinal assms(1))
from assms show "A ⊆⇩∘ α"
by (meson Ord_α Ord_linear_le mem_not_refl vsubsetE)
from assms(1) this interpret A: cat_linear_order α ‹cat_ordinal A›
by (intro cat_linear_order_cat_ordinal)
from assms(2) have A_in_Vset: "A ∈⇩∘ Vset α" by (simp add: Ord_α Ord_in_in_VsetI)
have "cat_ordinal A⦇Arr⦈ ⊆⇩∘ A ×⇩∙ A"
unfolding ordinal_arrs_def cat_ordinal_components by clarsimp
moreover from A_in_Vset have "A ×⇩∙ A ∈⇩∘ Vset α"
by (intro Limit_ftimes_in_VsetI) auto
ultimately have "cat_ordinal A⦇Arr⦈ ∈⇩∘ Vset α"
using vsubset_in_VsetI unfolding cat_ordinal_components by simp
moreover have "cat_ordinal A⦇Obj⦈ ∈⇩∘ Vset α"
unfolding cat_ordinal_components by (intro A_in_Vset)
ultimately show "tiny_category α (cat_ordinal A)"
by (cs_concl cs_shallow cs_intro: cat_cs_intros tiny_categoryI')
qed

lemmas [cat_ordinal_cs_intros] = 𝒵.cat_linear_order_cat_ordinal

lemma (in 𝒵) finite_category_cat_ordinal[cat_ordinal_cs_intros]:
assumes "a ∈⇩∘ ω"
shows "finite_category α (cat_ordinal a)"
proof-
from assms have "Ord a" "a ∈⇩∘ α" by (auto simp: Ord_α Ord_trans)
then interpret cat_ordinal: cat_tiny_linear_order α ‹cat_ordinal a›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
show ?thesis
proof(intro finite_categoryI')
from assms show "category α (cat_ordinal a)"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms show "vfinite (cat_ordinal a⦇Obj⦈)"
unfolding cat_ordinal_components by auto
from assms show "vfinite (cat_ordinal a⦇Arr⦈)"
proof-
have "cat_ordinal a⦇Arr⦈ ⊆⇩∘ a ×⇩∙ a"
unfolding cat_ordinal_components by auto
moreover from assms have "vfinite (a ×⇩∙ a)"
by (intro vfinite_ftimesI) auto
ultimately show ?thesis by (auto simp: vfinite_vsubset)
qed
qed
qed

lemmas [cat_ordinal_cs_intros] = 𝒵.finite_category_cat_ordinal

end```