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	fucinv 17901*	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 17902*	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 17903*	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 17904	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 17905	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 17906	Extend class notation with the class of initial objects of a category.
class InitO
Syntax	ctermo 17907	Extend class notation with the class of terminal objects of a category.
class TermO
Syntax	czeroo 17908	Extend class notation with the class of zero objects of a category.
class ZeroO
Definition	df-inito 17909*	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 17928 and dfinito3 17930 for alternate definitions depending on df-termo 17910. See dfinito4 49474 for an alternate definition using the universal property. (Contributed by AV, 3-Apr-2020.)
⊢ InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)})
Definition	df-termo 17910*	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 17929 and dftermo3 17931 for alternate definitions depending on df-inito 17909. See dftermo4 49475 for an alternate definition using the universal property. (Contributed by AV, 3-Apr-2020.)
⊢ TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)})
Definition	df-zeroo 17911	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 17912	InitO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO Fn Cat
Theorem	termofn 17913	TermO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO Fn Cat
Theorem	zeroofn 17914	ZeroO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ ZeroO Fn Cat
Theorem	initorcl 17915	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 17916	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 17917	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 17918*	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 17919*	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 17920	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 17921*	The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏)))
Theorem	istermo 17922*	The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼)))
Theorem	iszeroo 17923	The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶))))
Theorem	isinitoi 17924*	Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏)))
Theorem	istermoi 17925*	Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂)))
Theorem	initoid 17926	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 17927	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 17928	An initial object is a terminal object in the opposite category. An alternate definition of df-inito 17909 depending on df-termo 17910. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO = (𝑐 ∈ Cat ↦ (TermO‘(oppCat‘𝑐)))
Theorem	dftermo2 17929	A terminal object is an initial object in the opposite category. An alternate definition of df-termo 17910 depending on df-inito 17909. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO = (𝑐 ∈ Cat ↦ (InitO‘(oppCat‘𝑐)))
Theorem	dfinito3 17930	An alternate definition of df-inito 17909 depending on df-termo 17910, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO = (TermO ∘ (oppCat ↾ Cat))
Theorem	dftermo3 17931	An alternate definition of df-termo 17910 depending on df-inito 17909, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO = (InitO ∘ (oppCat ↾ Cat))
Theorem	initoo 17932	An initial object is an object. (Contributed by AV, 14-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	termoo 17933	A terminal object is an object. (Contributed by AV, 18-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	iszeroi 17934	Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶))))
Theorem	2initoinv 17935	Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	initoeu1 17936*	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 17937	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 17938	Lemma 0 for initoeu2 17941. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾))
Theorem	initoeu2lem1 17939*	Lemma 1 for initoeu2 17941. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)))
Theorem	initoeu2lem2 17940*	Lemma 2 for initoeu2 17941. (Contributed by AV, 10-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷)))
Theorem	initoeu2 17941	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 17942	Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	termoeu1 17943*	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 17944	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 17945	Extend class notation to include the domain extractor for an arrow.
class doma
Syntax	ccoda 17946	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 17947	Extend class notation to include the collection of all arrows of a category.
class Arrow
Syntax	choma 17948	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 17949	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 17950	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 17951*	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 17949 and df-coda 17950. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
Definition	df-arw 17952	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 17953	Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat)
Theorem	homafval 17954*	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥))))
Theorem	homaf 17955	Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V))
Theorem	homaval 17956	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = ({⟨𝑋, 𝑌⟩} × (𝑋𝐽𝑌)))
Theorem	elhoma 17957	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍(𝑋𝐻𝑌)𝐹 ↔ (𝑍 = ⟨𝑋, 𝑌⟩ ∧ 𝐹 ∈ (𝑋𝐽𝑌))))
Theorem	elhomai 17958	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩(𝑋𝐻𝑌)𝐹)
Theorem	elhomai2 17959	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌, 𝐹⟩ ∈ (𝑋𝐻𝑌))
Theorem	homarcl2 17960	Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
Theorem	homarel 17961	An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ Rel (𝑋𝐻𝑌)
Theorem	homa1 17962	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝑍 = ⟨𝑋, 𝑌⟩)
Theorem	homahom2 17963	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 17964	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 17965	The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋)
Theorem	homacd 17966	The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌)
Theorem	homadmcd 17967	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = ⟨𝑋, 𝑌, (2nd ‘𝐹)⟩)
Theorem	arwval 17968	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 17969	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 17970	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 17971	A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑋𝐻𝑌) ⊆ 𝐴
Theorem	arwdm 17972	The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵)
Theorem	arwcd 17973	The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (coda‘𝐹) ∈ 𝐵)
Theorem	dmaf 17974	The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (doma ↾ 𝐴):𝐴⟶𝐵
Theorem	cdaf 17975	The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (coda ↾ 𝐴):𝐴⟶𝐵
Theorem	arwhom 17976	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 17977	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 17978	Extend class notation to include identity for arrows.
class Ida
Syntax	ccoa 17979	Extend class notation to include composition for arrows.
class compa
Definition	df-ida 17980*	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 17981*	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 17982*	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ ⟨𝑥, 𝑥, ( 1 ‘𝑥)⟩))
Theorem	idaval 17983	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = ⟨𝑋, 𝑋, ( 1 ‘𝑋)⟩)
Theorem	ida2 17984	Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐼‘𝑋)) = ( 1 ‘𝑋))
Theorem	idahom 17985	Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐻𝑋))
Theorem	idadm 17986	Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (doma‘(𝐼‘𝑋)) = 𝑋)
Theorem	idacd 17987	Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (coda‘(𝐼‘𝑋)) = 𝑋)
Theorem	idaf 17988	The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼:𝐵⟶𝐴)
Theorem	coafval 17989*	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 17990	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‘𝐺)))
Theorem	dmcoass 17991	The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ dom · ⊆ (𝐴 × 𝐴)
Theorem	homdmcoa 17992	If 𝐹:𝑋⟶𝑌 and 𝐺:𝑌⟶𝑍, then 𝐺 and 𝐹 are composable. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → 𝐺dom · 𝐹)
Theorem	coaval 17993	Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (𝐺 · 𝐹) = ⟨𝑋, 𝑍, ((2nd ‘𝐺)(⟨𝑋, 𝑌⟩ ∙ 𝑍)(2nd ‘𝐹))⟩)
Theorem	coa2 17994	The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐺 · 𝐹)) = ((2nd ‘𝐺)(⟨𝑋, 𝑌⟩ ∙ 𝑍)(2nd ‘𝐹)))
Theorem	coahom 17995	The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺 · 𝐹) ∈ (𝑋𝐻𝑍))
Theorem	coapm 17996	Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ · ∈ (𝐴 ↑pm (𝐴 × 𝐴))
Theorem	arwlid 17997	Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (( 1 ‘𝑌) · 𝐹) = 𝐹)
Theorem	arwrid 17998	Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 𝐹)
Theorem	arwass 17999	Associativity of composition in a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → ((𝐾 · 𝐺) · 𝐹) = (𝐾 · (𝐺 · 𝐹)))
8.3  Examples of categories
8.3.1  The category of sets
Syntax	csetc 18000	Extend class notation to include the category Set.
class SetCat