P. 180 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17901-18000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fthres2b 17901*	Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (Subcat‘𝐷))    &   ⊢ (𝜑 → 𝑅 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹(𝐶 Faith (𝐷 ↾cat 𝑅))𝐺))
Theorem	fthres2c 17902	Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐸 = (𝐷 ↾s 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹(𝐶 Faith 𝐸)𝐺))
Theorem	fthres2 17903	A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝑅 ∈ (Subcat‘𝐷) → (𝐶 Faith (𝐷 ↾cat 𝑅)) ⊆ (𝐶 Faith 𝐷))
Theorem	idffth 17904	The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → 𝐼 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶)))
Theorem	cofull 17905	The composition of two full functors is full. Proposition 3.30(d) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Full 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Full 𝐸))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Full 𝐸))
Theorem	cofth 17906	The composition of two faithful functors is faithful. Proposition 3.30(c) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Faith 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Faith 𝐸))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Faith 𝐸))
Theorem	coffth 17907	The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ ((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷)))    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ ((𝐶 Full 𝐸) ∩ (𝐶 Faith 𝐸)))
Theorem	rescfth 17908	The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ 𝐼 = (idfunc‘𝐷)    ⇒   ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 ∈ (𝐷 Faith 𝐶))
Theorem	ressffth 17909	The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in [Adamek] p. 49. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾s 𝑆)    &   ⊢ 𝐼 = (idfunc‘𝐷)    ⇒   ⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶)))
Theorem	fullres2c 17910	Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐸 = (𝐷 ↾s 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ 𝐹(𝐶 Full 𝐸)𝐺))
Theorem	ffthres2c 17911	Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐸 = (𝐷 ↾s 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    ⇒   ⊢ (𝜑 → (𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺 ↔ 𝐹((𝐶 Full 𝐸) ∩ (𝐶 Faith 𝐸))𝐺))
Theorem	inclfusubc 17912*	The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ 𝑆 = (𝐶 ↾cat 𝐽)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = ( I ↾ 𝐵))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥𝐽𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑆 Func 𝐶)𝐺)
8.1.9  Natural transformations and the functor category
Syntax	cnat 17913	Extend class notation to include the collection of natural transformations.
class Nat
Syntax	cfuc 17914	Extend class notation to include the functor category.
class FuncCat
Definition	df-nat 17915*	Definition of a natural transformation between two functors. A natural transformation 𝐴:𝐹⟶𝐺 is a collection of arrows 𝐴(𝑥):𝐹(𝑥)⟶𝐺(𝑥), such that 𝐴(𝑦) ∘ 𝐹(ℎ) = 𝐺(ℎ) ∘ 𝐴(𝑥) for each morphism ℎ:𝑥⟶𝑦. Definition 6.1 in [Adamek] p. 83, and definition in [Lang] p. 65. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ Nat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}))
Definition	df-fuc 17916*	Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩})
Theorem	fnfuc 17917	The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ FuncCat Fn (Cat × Cat)
Theorem	natfval 17918*	Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    ⇒   ⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩ · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩ · (𝑠‘𝑦))(𝑎‘𝑥))})
Theorem	isnat 17919*	Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(⟨(𝐹‘𝑥), (𝐾‘𝑥)⟩ · (𝐾‘𝑦))(𝐴‘𝑥)))))
Theorem	isnat2 17920*	Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐹𝑁𝐺) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩ · ((1st ‘𝐺)‘𝑦))((𝑥(2nd ‘𝐹)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝐺)𝑦)‘ℎ)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ · ((1st ‘𝐺)‘𝑦))(𝐴‘𝑥)))))
Theorem	natffn 17921	The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷))
Theorem	natrcl 17922	Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ (𝐴 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)))
Theorem	nat1st2nd 17923	Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (⟨(1st ‘𝐹), (2nd ‘𝐹)⟩𝑁⟨(1st ‘𝐺), (2nd ‘𝐺)⟩))
Theorem	natixp 17924*	A natural transformation is a function from the objects of 𝐶 to homomorphisms from 𝐹(𝑥) to 𝐺(𝑥). (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)))
Theorem	natcl 17925	A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) ∈ ((𝐹‘𝑋)𝐽(𝐾‘𝑋)))
Theorem	natfn 17926	A natural transformation is a function on the objects of 𝐶. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → 𝐴 Fn 𝐵)
Theorem	nati 17927	Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝐴‘𝑌)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩ · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹‘𝑋), (𝐾‘𝑋)⟩ · (𝐾‘𝑌))(𝐴‘𝑋)))
Theorem	wunnat 17928	A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈)
Theorem	catstr 17929	A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ {⟨(Base‘ndx), 𝑈⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} Struct ⟨1, ;15⟩
Theorem	fucval 17930*	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (𝐶 Func 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩ · ((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))))    ⇒   ⊢ (𝜑 → 𝑄 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), ∙ ⟩})
Theorem	fuccofval 17931*	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (𝐶 Func 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ ∙ = (comp‘𝑄)    ⇒   ⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩ · ((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))))
Theorem	fucbas 17932	The objects of the functor category are functors from 𝐶 to 𝐷. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    ⇒   ⊢ (𝐶 Func 𝐷) = (Base‘𝑄)
Theorem	fuchom 17933	The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ 𝑁 = (Hom ‘𝑄)
Theorem	fucco 17934*	Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    ⇒   ⊢ (𝜑 → (𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ · ((1st ‘𝐻)‘𝑥))(𝑅‘𝑥))))
Theorem	fuccoval 17935	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅)‘𝑋) = ((𝑆‘𝑋)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩ · ((1st ‘𝐻)‘𝑋))(𝑅‘𝑋)))
Theorem	fuccocl 17936	The composition of two natural transformations is a natural transformation. Remark 6.14(a) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    ⇒   ⊢ (𝜑 → (𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅) ∈ (𝐹𝑁𝐻))
Theorem	fucidcl 17937	The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( 1 ∘ (1st ‘𝐹)) ∈ (𝐹𝑁𝐹))
Theorem	fuclid 17938	Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → (( 1 ∘ (1st ‘𝐺))(⟨𝐹, 𝐺⟩ ∙ 𝐺)𝑅) = 𝑅)
Theorem	fucrid 17939	Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → (𝑅(⟨𝐹, 𝐹⟩ ∙ 𝐺)( 1 ∘ (1st ‘𝐹))) = 𝑅)
Theorem	fucass 17940	Associativity of natural transformation composition. Remark 6.14(b) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ (𝐻𝑁𝐾))    ⇒   ⊢ (𝜑 → ((𝑇(⟨𝐺, 𝐻⟩ ∙ 𝐾)𝑆)(⟨𝐹, 𝐺⟩ ∙ 𝐾)𝑅) = (𝑇(⟨𝐹, 𝐻⟩ ∙ 𝐾)(𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅)))
Theorem	fuccatid 17941*	The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 1 = (Id‘𝐷)    ⇒   ⊢ (𝜑 → (𝑄 ∈ Cat ∧ (Id‘𝑄) = (𝑓 ∈ (𝐶 Func 𝐷) ↦ ( 1 ∘ (1st ‘𝑓)))))
Theorem	fuccat 17942	The functor category is a category. Remark 6.16 in [Adamek] p. 88. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ Cat)
Theorem	fucid 17943	The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1st ‘𝐹)))
Theorem	fucsect 17944*	Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝑆 = (Sect‘𝑄)    &   ⊢ 𝑇 = (Sect‘𝐷)    ⇒   ⊢ (𝜑 → (𝑈(𝐹𝑆𝐺)𝑉 ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ 𝑉 ∈ (𝐺𝑁𝐹) ∧ ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝑇((1st ‘𝐺)‘𝑥))(𝑉‘𝑥))))
Theorem	fucinv 17945*	Two natural transformations are inverses of each other iff all the components are inverse. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝐼 = (Inv‘𝑄)    &   ⊢ 𝐽 = (Inv‘𝐷)    ⇒   ⊢ (𝜑 → (𝑈(𝐹𝐼𝐺)𝑉 ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ 𝑉 ∈ (𝐺𝑁𝐹) ∧ ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))(𝑉‘𝑥))))
Theorem	invfuc 17946*	If 𝑉(𝑥) is an inverse to 𝑈(𝑥) for each 𝑥, and 𝑈 is a natural transformation, then 𝑉 is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝐼 = (Inv‘𝑄)    &   ⊢ 𝐽 = (Inv‘𝐷)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐹𝑁𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))𝑋)    ⇒   ⊢ (𝜑 → 𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋))
Theorem	fuciso 17947*	A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝐼 = (Iso‘𝑄)    &   ⊢ 𝐽 = (Iso‘𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐹𝐼𝐺) ↔ (𝐴 ∈ (𝐹𝑁𝐺) ∧ ∀𝑥 ∈ 𝐵 (𝐴‘𝑥) ∈ (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)))))
Theorem	natpropd 17948	If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ Cat)    &   ⊢ (𝜑 → 𝐵 ∈ Cat)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (𝐴 Nat 𝐶) = (𝐵 Nat 𝐷))
Theorem	fucpropd 17949	If two categories have the same set of objects, morphisms, and compositions, then they have the same functor categories. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ Cat)    &   ⊢ (𝜑 → 𝐵 ∈ Cat)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (𝐴 FuncCat 𝐶) = (𝐵 FuncCat 𝐷))
8.1.10  Initial, terminal and zero objects of a category
Syntax	cinito 17950	Extend class notation with the class of initial objects of a category.
class InitO
Syntax	ctermo 17951	Extend class notation with the class of terminal objects of a category.
class TermO
Syntax	czeroo 17952	Extend class notation with the class of zero objects of a category.
class ZeroO
Definition	df-inito 17953*	An object A is said to be an initial object provided that for each object B there is exactly one morphism from A to B. Definition 7.1 in [Adamek] p. 101, or definition in [Lang] p. 57 (called "a universally repelling object" there). See dfinito2 17972 and dfinito3 17974 for alternate definitions depending on df-termo 17954. See dfinito4 49494 for an alternate definition using the universal property. (Contributed by AV, 3-Apr-2020.)
⊢ InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)})
Definition	df-termo 17954*	An object A is called a terminal object provided that for each object B there is exactly one morphism from B to A. Definition 7.4 in [Adamek] p. 102, or definition in [Lang] p. 57 (called "a universally attracting object" there). See dftermo2 17973 and dftermo3 17975 for alternate definitions depending on df-inito 17953. See dftermo4 49495 for an alternate definition using the universal property. (Contributed by AV, 3-Apr-2020.)
⊢ TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)})
Definition	df-zeroo 17955	An object A is called a zero object provided that it is both an initial object and a terminal object. Definition 7.7 of [Adamek] p. 103. (Contributed by AV, 3-Apr-2020.)
⊢ ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))
Theorem	initofn 17956	InitO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO Fn Cat
Theorem	termofn 17957	TermO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO Fn Cat
Theorem	zeroofn 17958	ZeroO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ ZeroO Fn Cat
Theorem	initorcl 17959	Reverse closure for an initial object: If a class has an initial object, the class is a category. (Contributed by AV, 4-Apr-2020.)
⊢ (𝐼 ∈ (InitO‘𝐶) → 𝐶 ∈ Cat)
Theorem	termorcl 17960	Reverse closure for a terminal object: If a class has a terminal object, the class is a category. (Contributed by AV, 4-Apr-2020.)
⊢ (𝑇 ∈ (TermO‘𝐶) → 𝐶 ∈ Cat)
Theorem	zeroorcl 17961	Reverse closure for a zero object: If a class has a zero object, the class is a category. (Contributed by AV, 4-Apr-2020.)
⊢ (𝑍 ∈ (ZeroO‘𝐶) → 𝐶 ∈ Cat)
Theorem	initoval 17962*	The value of the initial object function, i.e. the set of all initial objects of a category. (Contributed by AV, 3-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (InitO‘𝐶) = {𝑎 ∈ 𝐵 ∣ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑎𝐻𝑏)})
Theorem	termoval 17963*	The value of the terminal object function, i.e. the set of all terminal objects of a category. (Contributed by AV, 3-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (TermO‘𝐶) = {𝑎 ∈ 𝐵 ∣ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑎)})
Theorem	zerooval 17964	The value of the zero object function, i.e. the set of all zero objects of a category. (Contributed by AV, 3-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (ZeroO‘𝐶) = ((InitO‘𝐶) ∩ (TermO‘𝐶)))
Theorem	isinito 17965*	The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏)))
Theorem	istermo 17966*	The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼)))
Theorem	iszeroo 17967	The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶))))
Theorem	isinitoi 17968*	Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏)))
Theorem	istermoi 17969*	Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂)))
Theorem	initoid 17970	For an initial object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 6-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})
Theorem	termoid 17971	For a terminal object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 18-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})
Theorem	dfinito2 17972	An initial object is a terminal object in the opposite category. An alternate definition of df-inito 17953 depending on df-termo 17954. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO = (𝑐 ∈ Cat ↦ (TermO‘(oppCat‘𝑐)))
Theorem	dftermo2 17973	A terminal object is an initial object in the opposite category. An alternate definition of df-termo 17954 depending on df-inito 17953. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO = (𝑐 ∈ Cat ↦ (InitO‘(oppCat‘𝑐)))
Theorem	dfinito3 17974	An alternate definition of df-inito 17953 depending on df-termo 17954, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO = (TermO ∘ (oppCat ↾ Cat))
Theorem	dftermo3 17975	An alternate definition of df-termo 17954 depending on df-inito 17953, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO = (InitO ∘ (oppCat ↾ Cat))
Theorem	initoo 17976	An initial object is an object. (Contributed by AV, 14-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	termoo 17977	A terminal object is an object. (Contributed by AV, 18-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	iszeroi 17978	Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶))))
Theorem	2initoinv 17979	Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	initoeu1 17980*	Initial objects are essentially unique (strong form), i.e. there is a unique isomorphism between two initial objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 14-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
Theorem	initoeu1w 17981	Initial objects are essentially unique (weak form), i.e. if A and B are initial objects, then A and B are isomorphic. Proposition 7.3 (1) of [Adamek] p. 102. (Contributed by AV, 6-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ (𝜑 → 𝐴( ≃𝑐 ‘𝐶)𝐵)
Theorem	initoeu2lem0 17982	Lemma 0 for initoeu2 17985. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾))
Theorem	initoeu2lem1 17983*	Lemma 1 for initoeu2 17985. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)))
Theorem	initoeu2lem2 17984*	Lemma 2 for initoeu2 17985. (Contributed by AV, 10-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷)))
Theorem	initoeu2 17985	Initial objects are essentially unique, if A is an initial object, then so is every object that is isomorphic to A. Proposition 7.3 (2) in [Adamek] p. 102. (Contributed by AV, 10-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐴( ≃𝑐 ‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))
Theorem	2termoinv 17986	Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	termoeu1 17987*	Terminal objects are essentially unique (strong form), i.e. there is a unique isomorphism between two terminal objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
Theorem	termoeu1w 17988	Terminal objects are essentially unique (weak form), i.e. if A and B are terminal objects, then A and B are isomorphic. Proposition 7.6 of [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ (𝜑 → 𝐴( ≃𝑐 ‘𝐶)𝐵)
8.2  Arrows (disjointified hom-sets)
Syntax	cdoma 17989	Extend class notation to include the domain extractor for an arrow.
class doma
Syntax	ccoda 17990	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 17991	Extend class notation to include the collection of all arrows of a category.
class Arrow
Syntax	choma 17992	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 17993	Definition of the domain extractor for an arrow. (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ doma = (1st ∘ 1st )
Definition	df-coda 17994	Definition of the codomain extractor for an arrow. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ coda = (2nd ∘ 1st )
Definition	df-homa 17995*	Definition of the hom-set extractor for arrows, which tags the morphisms of the underlying hom-set with domain and codomain, which can then be extracted using df-doma 17993 and df-coda 17994. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
Definition	df-arw 17996	Definition of the set of arrows of a category. We will use the term "arrow" to denote a morphism tagged with its domain and codomain, as opposed to Hom, which allows hom-sets for distinct objects to overlap. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ Arrow = (𝑐 ∈ Cat ↦ ∪ ran (Homa‘𝑐))
Theorem	homarcl 17997	Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat)
Theorem	homafval 17998*	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥))))
Theorem	homaf 17999	Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V))
Theorem	homaval 18000	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = ({⟨𝑋, 𝑌⟩} × (𝑋𝐽𝑌)))