P. 171 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17001-17100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wunnat 17001	A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈)
Theorem	catstr 17002	A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ {⟨(Base‘ndx), 𝑈⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} Struct ⟨1, ;15⟩
Theorem	fucval 17003*	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 17004*	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 17005	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 17006	The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ 𝑁 = (Hom ‘𝑄)
Theorem	fucco 17007*	Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    ⇒   ⊢ (𝜑 → (𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ · ((1st ‘𝐻)‘𝑥))(𝑅‘𝑥))))
Theorem	fuccoval 17008	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅)‘𝑋) = ((𝑆‘𝑋)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩ · ((1st ‘𝐻)‘𝑋))(𝑅‘𝑋)))
Theorem	fuccocl 17009	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 17010	The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( 1 ∘ (1st ‘𝐹)) ∈ (𝐹𝑁𝐹))
Theorem	fuclid 17011	Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → (( 1 ∘ (1st ‘𝐺))(⟨𝐹, 𝐺⟩ ∙ 𝐺)𝑅) = 𝑅)
Theorem	fucrid 17012	Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → (𝑅(⟨𝐹, 𝐹⟩ ∙ 𝐺)( 1 ∘ (1st ‘𝐹))) = 𝑅)
Theorem	fucass 17013	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 17014*	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 17015	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 17016	The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1st ‘𝐹)))
Theorem	fucsect 17017*	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 17018*	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 17019*	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 17020*	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 17021	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 17022	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 17023	Extend class notation with the class of initial objects of a category.
class InitO
Syntax	ctermo 17024	Extend class notation with the class of terminal objects of a category.
class TermO
Syntax	czeroo 17025	Extend class notation with the class of zero objects of a category.
class ZeroO
Definition	df-inito 17026*	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). (Contributed by AV, 3-Apr-2020.)
⊢ InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)})
Definition	df-termo 17027*	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). (Contributed by AV, 3-Apr-2020.)
⊢ TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)})
Definition	df-zeroo 17028	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	initorcl 17029	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 17030	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 17031	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 17032*	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 17033*	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 17034	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 17035*	The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏)))
Theorem	istermo 17036*	The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼)))
Theorem	iszeroo 17037	The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶))))
Theorem	isinitoi 17038*	Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏)))
Theorem	istermoi 17039*	Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂)))
Theorem	initoid 17040	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 17041	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	initoo 17042	An initial object is an object. (Contributed by AV, 14-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	termoo 17043	A terminal object is an object. (Contributed by AV, 18-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	iszeroi 17044	Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶))))
Theorem	2initoinv 17045	Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	initoeu1 17046*	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 17047	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 17048	Lemma 0 for initoeu2 17051. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾))
Theorem	initoeu2lem1 17049*	Lemma 1 for initoeu2 17051. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)))
Theorem	initoeu2lem2 17050*	Lemma 2 for initoeu2 17051. (Contributed by AV, 10-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷)))
Theorem	initoeu2 17051	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 17052	Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	termoeu1 17053*	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 17054	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 17055	Extend class notation to include the domain extractor for an arrow.
class doma
Syntax	ccoda 17056	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 17057	Extend class notation to include the collection of all arrows of a category.
class Arrow
Syntax	choma 17058	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 17059	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 17060	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 17061*	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 17059 and df-coda 17060. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
Definition	df-arw 17062	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 17063	Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat)
Theorem	homafval 17064*	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥))))
Theorem	homaf 17065	Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V))
Theorem	homaval 17066	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = ({⟨𝑋, 𝑌⟩} × (𝑋𝐽𝑌)))
Theorem	elhoma 17067	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍(𝑋𝐻𝑌)𝐹 ↔ (𝑍 = ⟨𝑋, 𝑌⟩ ∧ 𝐹 ∈ (𝑋𝐽𝑌))))
Theorem	elhomai 17068	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩(𝑋𝐻𝑌)𝐹)
Theorem	elhomai2 17069	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌, 𝐹⟩ ∈ (𝑋𝐻𝑌))
Theorem	homarcl2 17070	Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
Theorem	homarel 17071	An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ Rel (𝑋𝐻𝑌)
Theorem	homa1 17072	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝑍 = ⟨𝑋, 𝑌⟩)
Theorem	homahom2 17073	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝐹 ∈ (𝑋𝐽𝑌))
Theorem	homahom 17074	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (2nd ‘𝐹) ∈ (𝑋𝐽𝑌))
Theorem	homadm 17075	The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋)
Theorem	homacd 17076	The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌)
Theorem	homadmcd 17077	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = ⟨𝑋, 𝑌, (2nd ‘𝐹)⟩)
Theorem	arwval 17078	The set of arrows is the union of all the disjointified hom-sets. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ 𝐴 = ∪ ran 𝐻
Theorem	arwrcl 17079	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐶 ∈ Cat)
Theorem	arwhoma 17080	An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹 ∈ ((doma‘𝐹)𝐻(coda‘𝐹)))
Theorem	homarw 17081	A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑋𝐻𝑌) ⊆ 𝐴
Theorem	arwdm 17082	The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵)
Theorem	arwcd 17083	The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (coda‘𝐹) ∈ 𝐵)
Theorem	dmaf 17084	The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (doma ↾ 𝐴):𝐴⟶𝐵
Theorem	cdaf 17085	The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (coda ↾ 𝐴):𝐴⟶𝐵
Theorem	arwhom 17086	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (2nd ‘𝐹) ∈ ((doma‘𝐹)𝐽(coda‘𝐹)))
Theorem	arwdmcd 17087	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹 = ⟨(doma‘𝐹), (coda‘𝐹), (2nd ‘𝐹)⟩)
8.2.1  Identity and composition for arrows
Syntax	cida 17088	Extend class notation to include identity for arrows.
class Ida
Syntax	ccoa 17089	Extend class notation to include composition for arrows.
class compa
Definition	df-ida 17090*	Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
Definition	df-coa 17091*	Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a quinary operation like the regular composition in a category comp. Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ compa = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))⟩))
Theorem	idafval 17092*	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ ⟨𝑥, 𝑥, ( 1 ‘𝑥)⟩))
Theorem	idaval 17093	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = ⟨𝑋, 𝑋, ( 1 ‘𝑋)⟩)
Theorem	ida2 17094	Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐼‘𝑋)) = ( 1 ‘𝑋))
Theorem	idahom 17095	Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐻𝑋))
Theorem	idadm 17096	Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (doma‘(𝐼‘𝑋)) = 𝑋)
Theorem	idacd 17097	Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (coda‘(𝐼‘𝑋)) = 𝑋)
Theorem	idaf 17098	The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼:𝐵⟶𝐴)
Theorem	coafval 17099*	The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ · = (𝑔 ∈ 𝐴, 𝑓 ∈ {ℎ ∈ 𝐴 ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩ ∙ (coda‘𝑔))(2nd ‘𝑓))⟩)
Theorem	eldmcoa 17100	A pair ⟨𝐺, 𝐹⟩ is in the domain of the arrow composition, if the domain of 𝐺 equals the codomain of 𝐹. (In this case we say 𝐺 and 𝐹 are composable.) (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝐺dom · 𝐹 ↔ (𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (coda‘𝐹) = (doma‘𝐺)))