P. 182 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18101-18200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	termoeu1w 18101	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 18102	Extend class notation to include the domain extractor for an arrow.
class doma
Syntax	ccoda 18103	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 18104	Extend class notation to include the collection of all arrows of a category.
class Arrow
Syntax	choma 18105	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 18106	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 18107	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 18108*	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 18106 and df-coda 18107. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
Definition	df-arw 18109	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 18110	Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat)
Theorem	homafval 18111*	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥))))
Theorem	homaf 18112	Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V))
Theorem	homaval 18113	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = ({⟨𝑋, 𝑌⟩} × (𝑋𝐽𝑌)))
Theorem	elhoma 18114	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍(𝑋𝐻𝑌)𝐹 ↔ (𝑍 = ⟨𝑋, 𝑌⟩ ∧ 𝐹 ∈ (𝑋𝐽𝑌))))
Theorem	elhomai 18115	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩(𝑋𝐻𝑌)𝐹)
Theorem	elhomai2 18116	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌, 𝐹⟩ ∈ (𝑋𝐻𝑌))
Theorem	homarcl2 18117	Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
Theorem	homarel 18118	An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ Rel (𝑋𝐻𝑌)
Theorem	homa1 18119	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝑍 = ⟨𝑋, 𝑌⟩)
Theorem	homahom2 18120	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 18121	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 18122	The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋)
Theorem	homacd 18123	The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌)
Theorem	homadmcd 18124	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = ⟨𝑋, 𝑌, (2nd ‘𝐹)⟩)
Theorem	arwval 18125	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 18126	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 18127	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 18128	A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑋𝐻𝑌) ⊆ 𝐴
Theorem	arwdm 18129	The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵)
Theorem	arwcd 18130	The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (coda‘𝐹) ∈ 𝐵)
Theorem	dmaf 18131	The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (doma ↾ 𝐴):𝐴⟶𝐵
Theorem	cdaf 18132	The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (coda ↾ 𝐴):𝐴⟶𝐵
Theorem	arwhom 18133	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 18134	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 18135	Extend class notation to include identity for arrows.
class Ida
Syntax	ccoa 18136	Extend class notation to include composition for arrows.
class compa
Definition	df-ida 18137*	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 18138*	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 18139*	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ ⟨𝑥, 𝑥, ( 1 ‘𝑥)⟩))
Theorem	idaval 18140	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = ⟨𝑋, 𝑋, ( 1 ‘𝑋)⟩)
Theorem	ida2 18141	Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐼‘𝑋)) = ( 1 ‘𝑋))
Theorem	idahom 18142	Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐻𝑋))
Theorem	idadm 18143	Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (doma‘(𝐼‘𝑋)) = 𝑋)
Theorem	idacd 18144	Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (coda‘(𝐼‘𝑋)) = 𝑋)
Theorem	idaf 18145	The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼:𝐵⟶𝐴)
Theorem	coafval 18146*	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 18147	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 18148	The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ dom · ⊆ (𝐴 × 𝐴)
Theorem	homdmcoa 18149	If 𝐹:𝑋⟶𝑌 and 𝐺:𝑌⟶𝑍, then 𝐺 and 𝐹 are composable. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → 𝐺dom · 𝐹)
Theorem	coaval 18150	Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (𝐺 · 𝐹) = ⟨𝑋, 𝑍, ((2nd ‘𝐺)(⟨𝑋, 𝑌⟩ ∙ 𝑍)(2nd ‘𝐹))⟩)
Theorem	coa2 18151	The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐺 · 𝐹)) = ((2nd ‘𝐺)(⟨𝑋, 𝑌⟩ ∙ 𝑍)(2nd ‘𝐹)))
Theorem	coahom 18152	The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺 · 𝐹) ∈ (𝑋𝐻𝑍))
Theorem	coapm 18153	Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ · ∈ (𝐴 ↑pm (𝐴 × 𝐴))
Theorem	arwlid 18154	Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (( 1 ‘𝑌) · 𝐹) = 𝐹)
Theorem	arwrid 18155	Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 𝐹)
Theorem	arwass 18156	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 18157	Extend class notation to include the category Set.
class SetCat
Definition	df-setc 18158*	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 18159*	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 18160	Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
Theorem	setchomfval 18161*	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ (𝑦 ↑m 𝑥)))
Theorem	setchom 18162	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑌 ↑m 𝑋))
Theorem	elsetchom 18163	A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ↔ 𝐹:𝑋⟶𝑌))
Theorem	setccofval 18164*	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))
Theorem	setcco 18165	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑍)    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	setccatid 18166*	Lemma for setccat 18167. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥))))
Theorem	setccat 18167	The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	setcid 18168	The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑋))
Theorem	setcmon 18169	A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ 𝐹:𝑋–1-1→𝑌))
Theorem	setcepi 18170	An epimorphism of sets is a surjection. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 2o ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋–onto→𝑌))
Theorem	setcsect 18171	A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹:𝑋⟶𝑌 ∧ 𝐺:𝑌⟶𝑋 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝑋))))
Theorem	setcinv 18172	An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ 𝐺 = ◡𝐹)))
Theorem	setciso 18173	An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹:𝑋–1-1-onto→𝑌))
Theorem	resssetc 18174	The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCat‘𝑈 categories for different 𝑈 are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ 𝐷 = (SetCat‘𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((Homf ‘(𝐶 ↾s 𝑉)) = (Homf ‘𝐷) ∧ (compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷)))
Theorem	funcsetcres2 18175	A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ 𝐷 = (SetCat‘𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → (𝐸 Func 𝐷) ⊆ (𝐸 Func 𝐶))
Theorem	setc2obas 18176	∅ and 1o are distinct objects in (SetCat‘2o). This combined with setc2ohom 18177 demonstrates that the category does not have pairwise disjoint hom-sets. See also df-cat 17749 and cat1 18179. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ 𝐶 = (SetCat‘2o)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (∅ ∈ 𝐵 ∧ 1o ∈ 𝐵 ∧ 1o ≠ ∅)
Theorem	setc2ohom 18177	(SetCat‘2o) is a category (provable from setccat 18167 and 2oex 8474) that does not have pairwise disjoint hom-sets, proved by this theorem combined with setc2obas 18176. Notably, the empty set ∅ is simultaneously an object (setc2obas 18176), an identity morphism from ∅ to ∅ (setcid 18168 or thincid 50250), and a non-identity morphism from ∅ to 1o. See cat1lem 18178 and cat1 18179 for a more general statement. This category is also thin (setc2othin 50284), and therefore is "equivalent" to a preorder (actually a partial order). See prsthinc 50282 for more details on the "equivalence". (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ 𝐶 = (SetCat‘2o)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ ∅ ∈ ((∅𝐻∅) ∩ (∅𝐻1o))
Theorem	cat1lem 18178*	The category of sets in a "universe" containing the empty set and another set does not have pairwise disjoint hom-sets as required in Axiom CAT 1 in [Lang] p. 53. Lemma for cat1 18179. (Contributed by Zhi Wang, 15-Sep-2024.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → ∅ ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → ∅ ≠ 𝑌)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((𝑥𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
Theorem	cat1 18179*	The definition of category df-cat 17749 does not impose pairwise disjoint hom-sets as required in Axiom CAT 1 in [Lang] p. 53. See setc2obas 18176 and setc2ohom 18177 for a counterexample. For a version with pairwise disjoint hom-sets, see df-homa 18108 and its subsection. (Contributed by Zhi Wang, 15-Sep-2024.)
⊢ ∃𝑐 ∈ Cat [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ] ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))
8.3.2  The category of categories
Syntax	ccatc 18180	Extend class notation to include the category Cat.
class CatCat
Definition	df-catc 18181*	Definition of the category Cat, which consists of all categories in the universe 𝑢 (i.e., "𝑢-small categories", see Definition 3.44. of [Adamek] p. 39), with functors as the morphisms (catchom 18185, elcatchom 50215). Definition 3.47 of [Adamek] p. 40. We do not introduce a specific definition for "𝑢-large categories", which can be expressed as (Cat ∖ 𝑢). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ CatCat = (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Cat) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))⟩})
Theorem	catcval 18182*	Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦)))    &   ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	catcbas 18183	Set of objects of the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
Theorem	catchomfval 18184*	Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦)))
Theorem	catchom 18185	Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 Func 𝑌))
Theorem	catccofval 18186*	Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))))
Theorem	catcco 18187	Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋 Func 𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌 Func 𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘func 𝐹))
Theorem	catccatid 18188*	Lemma for catccat 18190. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ (idfunc‘𝑥))))
Theorem	catcid 18189	The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝐼 = (idfunc‘𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = 𝐼)
Theorem	catccat 18190	The category of categories is a category, see remark 3.48 in [Adamek] p. 40. (Clearly it cannot be an element of itself, hence it is "𝑈 -large".) (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	resscatc 18191	The restriction of the category of categories to a subset is the category of categories in the subset. Thus, the CatCat‘𝑈 categories for different 𝑈 are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐷 = (CatCat‘𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((Homf ‘(𝐶 ↾s 𝑉)) = (Homf ‘𝐷) ∧ (compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷)))
Theorem	catcisolem 18192*	Lemma for catciso 18193. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Inv‘𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ◡((◡𝐹‘𝑥)𝐺(◡𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)    &   ⊢ (𝜑 → 𝐹:𝑅–1-1-onto→𝑆)    ⇒   ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨◡𝐹, 𝐻⟩)
Theorem	catciso 18193	A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in [Adamek] p. 34. Note that "catciso.u" is redundant thanks to elbasfv 17300. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)))
Theorem	catcbascl 18194	An element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18199. (Contributed by AV, 14-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑈)
Theorem	catcslotelcl 18195	A slot entry of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18199. (Contributed by AV, 14-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝑈)
Theorem	catcbaselcl 18196	The base set of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18199. (Contributed by AV, 14-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈)
Theorem	catchomcl 18197	The Hom-set of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18199. (Contributed by AV, 14-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (Hom ‘𝑋) ∈ 𝑈)
Theorem	catcccocl 18198	The composition operation of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18199. (Contributed by AV, 14-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (comp‘𝑋) ∈ 𝑈)
Theorem	catcoppccl 18199	The category of categories for a weak universe is closed under taking opposites. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑂 ∈ 𝐵)
Theorem	catcfuccl 18200	The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑄 = (𝑋 FuncCat 𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑄 ∈ 𝐵)