P. 181 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18001-18100   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-termo 18001*	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 18020 and dftermo3 18022 for alternate definitions depending on df-inito 18000. See dftermo4 50087 for an alternate definition using the universal property. (Contributed by AV, 3-Apr-2020.)
⊢ TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)})
Definition	df-zeroo 18002	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 18003	InitO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO Fn Cat
Theorem	termofn 18004	TermO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO Fn Cat
Theorem	zeroofn 18005	ZeroO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ ZeroO Fn Cat
Theorem	initorcl 18006	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 18007	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 18008	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 18009*	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 18010*	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 18011	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 18012*	The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏)))
Theorem	istermo 18013*	The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼)))
Theorem	iszeroo 18014	The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶))))
Theorem	isinitoi 18015*	Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏)))
Theorem	istermoi 18016*	Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂)))
Theorem	initoid 18017	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 18018	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 18019	An initial object is a terminal object in the opposite category. An alternate definition of df-inito 18000 depending on df-termo 18001. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO = (𝑐 ∈ Cat ↦ (TermO‘(oppCat‘𝑐)))
Theorem	dftermo2 18020	A terminal object is an initial object in the opposite category. An alternate definition of df-termo 18001 depending on df-inito 18000. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO = (𝑐 ∈ Cat ↦ (InitO‘(oppCat‘𝑐)))
Theorem	dfinito3 18021	An alternate definition of df-inito 18000 depending on df-termo 18001, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO = (TermO ∘ (oppCat ↾ Cat))
Theorem	dftermo3 18022	An alternate definition of df-termo 18001 depending on df-inito 18000, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO = (InitO ∘ (oppCat ↾ Cat))
Theorem	initoo 18023	An initial object is an object. (Contributed by AV, 14-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	termoo 18024	A terminal object is an object. (Contributed by AV, 18-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	iszeroi 18025	Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶))))
Theorem	2initoinv 18026	Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	initoeu1 18027*	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 18028	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 18029	Lemma 0 for initoeu2 18032. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾))
Theorem	initoeu2lem1 18030*	Lemma 1 for initoeu2 18032. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)))
Theorem	initoeu2lem2 18031*	Lemma 2 for initoeu2 18032. (Contributed by AV, 10-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷)))
Theorem	initoeu2 18032	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 18033	Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	termoeu1 18034*	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 18035	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 18036	Extend class notation to include the domain extractor for an arrow.
class doma
Syntax	ccoda 18037	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 18038	Extend class notation to include the collection of all arrows of a category.
class Arrow
Syntax	choma 18039	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 18040	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 18041	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 18042*	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 18040 and df-coda 18041. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
Definition	df-arw 18043	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 18044	Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat)
Theorem	homafval 18045*	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥))))
Theorem	homaf 18046	Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V))
Theorem	homaval 18047	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = ({⟨𝑋, 𝑌⟩} × (𝑋𝐽𝑌)))
Theorem	elhoma 18048	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍(𝑋𝐻𝑌)𝐹 ↔ (𝑍 = ⟨𝑋, 𝑌⟩ ∧ 𝐹 ∈ (𝑋𝐽𝑌))))
Theorem	elhomai 18049	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩(𝑋𝐻𝑌)𝐹)
Theorem	elhomai2 18050	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌, 𝐹⟩ ∈ (𝑋𝐻𝑌))
Theorem	homarcl2 18051	Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
Theorem	homarel 18052	An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ Rel (𝑋𝐻𝑌)
Theorem	homa1 18053	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝑍 = ⟨𝑋, 𝑌⟩)
Theorem	homahom2 18054	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 18055	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 18056	The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋)
Theorem	homacd 18057	The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌)
Theorem	homadmcd 18058	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = ⟨𝑋, 𝑌, (2nd ‘𝐹)⟩)
Theorem	arwval 18059	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 18060	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 18061	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 18062	A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑋𝐻𝑌) ⊆ 𝐴
Theorem	arwdm 18063	The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵)
Theorem	arwcd 18064	The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (coda‘𝐹) ∈ 𝐵)
Theorem	dmaf 18065	The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (doma ↾ 𝐴):𝐴⟶𝐵
Theorem	cdaf 18066	The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (coda ↾ 𝐴):𝐴⟶𝐵
Theorem	arwhom 18067	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 18068	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 18069	Extend class notation to include identity for arrows.
class Ida
Syntax	ccoa 18070	Extend class notation to include composition for arrows.
class compa
Definition	df-ida 18071*	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 18072*	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 18073*	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ ⟨𝑥, 𝑥, ( 1 ‘𝑥)⟩))
Theorem	idaval 18074	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = ⟨𝑋, 𝑋, ( 1 ‘𝑋)⟩)
Theorem	ida2 18075	Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐼‘𝑋)) = ( 1 ‘𝑋))
Theorem	idahom 18076	Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐻𝑋))
Theorem	idadm 18077	Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (doma‘(𝐼‘𝑋)) = 𝑋)
Theorem	idacd 18078	Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (coda‘(𝐼‘𝑋)) = 𝑋)
Theorem	idaf 18079	The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼:𝐵⟶𝐴)
Theorem	coafval 18080*	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 18081	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 18082	The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ dom · ⊆ (𝐴 × 𝐴)
Theorem	homdmcoa 18083	If 𝐹:𝑋⟶𝑌 and 𝐺:𝑌⟶𝑍, then 𝐺 and 𝐹 are composable. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → 𝐺dom · 𝐹)
Theorem	coaval 18084	Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (𝐺 · 𝐹) = ⟨𝑋, 𝑍, ((2nd ‘𝐺)(⟨𝑋, 𝑌⟩ ∙ 𝑍)(2nd ‘𝐹))⟩)
Theorem	coa2 18085	The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐺 · 𝐹)) = ((2nd ‘𝐺)(⟨𝑋, 𝑌⟩ ∙ 𝑍)(2nd ‘𝐹)))
Theorem	coahom 18086	The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺 · 𝐹) ∈ (𝑋𝐻𝑍))
Theorem	coapm 18087	Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ · ∈ (𝐴 ↑pm (𝐴 × 𝐴))
Theorem	arwlid 18088	Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (( 1 ‘𝑌) · 𝐹) = 𝐹)
Theorem	arwrid 18089	Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 𝐹)
Theorem	arwass 18090	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 18091	Extend class notation to include the category Set.
class SetCat
Definition	df-setc 18092*	Definition of the category Set, relativized to a subset 𝑢. Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in 𝑢 and functions between these sets. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.)
⊢ SetCat = (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})
Theorem	setcval 18093*	Value of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ (𝑦 ↑m 𝑥)))    &   ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝑈⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	setcbas 18094	Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
Theorem	setchomfval 18095*	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ (𝑦 ↑m 𝑥)))
Theorem	setchom 18096	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑌 ↑m 𝑋))
Theorem	elsetchom 18097	A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ↔ 𝐹:𝑋⟶𝑌))
Theorem	setccofval 18098*	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))
Theorem	setcco 18099	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑍)    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	setccatid 18100*	Lemma for setccat 18101. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥))))