P. 493 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49201-49300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	thincfth 49201	A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
Theorem	thincciso 49202*	Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso.u" is redundant thanks to elbasfv 17221. (Contributed by Zhi Wang, 16-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆)))
Theorem	thinccisod 49203*	Two thin categories are isomorphic if the induced preorders are order-isomorphic (deduction form). Example 3.26(2) of [Adamek] p. 33. (Contributed by Zhi Wang, 22-Sep-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝑅–1-1-onto→𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝑥𝐻𝑦) = ∅ ↔ ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅))    ⇒   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)
Theorem	thincciso2 49204	Categories isomorphic to a thin category are thin. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso2.u" is redundant thanks to elbasfv 17221. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ThinCat)
Theorem	thincciso3 49205	Categories isomorphic to a thin category are thin. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso2.u" is redundant thanks to elbasfv 17221. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑌 ∈ ThinCat)
Theorem	thincciso4 49206	Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv 17221. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat))
Theorem	0thincg 49207	Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat)
Theorem	0thinc 49208	The empty category (see 0cat 17688) is thin. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ∅ ∈ ThinCat
Theorem	indthinc 49209*	An indiscrete category in which all hom-sets have exactly one morphism is a thin category. Constructed here is an indiscrete category where all morphisms are ∅. This is a special case of prsthinc 49211, where ≤ = (𝐵 × 𝐵). This theorem also implies a functor from the category of sets to the category of small categories. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof shortened by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	indthincALT 49210*	An alternate proof of indthinc 49209 assuming more axioms including ax-pow 5333 and ax-un 7724. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	prsthinc 49211*	Preordered sets as categories. Similar to example 3.3(4.d) of [Adamek] p. 24, but the hom-sets are not pairwise disjoint. One can define a functor from the category of prosets to the category of small thin categories. See catprs 48880 and catprs2 48881 for inducing a preorder from a category. Example 3.26(2) of [Adamek] p. 33 indicates that it induces a bijection from the equivalence class of isomorphic small thin categories to the equivalence class of order-isomorphic preordered sets. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	setcthin 49212*	A category of sets all of whose objects contain at most one element is thin. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (SetCat‘𝑈))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 ∃*𝑝 𝑝 ∈ 𝑥)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	setc2othin 49213	The category (SetCat‘2o) is thin. A special case of setcthin 49212. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (SetCat‘2o) ∈ ThinCat
Theorem	thincsect 49214	In a thin category, one morphism is a section of another iff they are pointing towards each other. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋))))
Theorem	thincsect2 49215	In a thin category, 𝐹 is a section of 𝐺 iff 𝐺 is a section of 𝐹. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ 𝐺(𝑌𝑆𝑋)𝐹))
Theorem	thincinv 49216	In a thin category, 𝐹 is an inverse of 𝐺 iff 𝐹 is a section of 𝐺 (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐹(𝑋𝑆𝑌)𝐺))
Theorem	thinciso 49217	In a thin category, 𝐹:𝑋⟶𝑌 is an isomorphism iff there is a morphism from 𝑌 to 𝑋. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ (𝑌𝐻𝑋) ≠ ∅))
Theorem	thinccic 49218	In a thin category, two objects are isomorphic iff there are morphisms between them in both directions. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ((𝑋𝐻𝑌) ≠ ∅ ∧ (𝑌𝐻𝑋) ≠ ∅)))
21.49.16.2  Terminal categories
Syntax	ctermc 49219	Extend class notation with the class of terminal categories.
class TermCat
Definition	df-termc 49220*	Definition of the proper class (termcnex 49314) of terminal categories, or final categories, i.e., categories with exactly one object and exactly one morphism, the latter of which is an identity morphism (termcid 49232). These are exactly the thin categories with a singleton base set. Example 3.3(4.c) of [Adamek] p. 24. As the name indicates, TermCat is the class of all terminal objects in the category of small categories (termcterm3 49261). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 49266). See also dftermc3 49277 where TermCat is defined as categories with exactly one disjointified arrow. Unlike https://ncatlab.org/nlab/show/terminal+category 49277, we reserve the term "trivial category" for (SetCat‘1o), justified by setc1oterm 49237. Followed directly from the definition, terminal categories are thin (termcthin 49224). The opposite category of a terminal category is "almost" itself (oppctermco 49251). Any category 𝐶 is isomorphic to the category of functors from a terminal category to the category 𝐶 (diagcic 49286). Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 49247) and terminal objects (dftermo4 49248). The universal properties provide an alternate proof of initoeu1 18011, termoeu1 18018, initoeu2 18016, and termoeu2 49018. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 49262). The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17687, 0thincg 49207, and 0funcg 48943. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
Theorem	istermc 49221*	The predicate "is a terminal category". A terminal category is a thin category with a singleton base set. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ ∃𝑥 𝐵 = {𝑥}))
Theorem	istermc2 49222*	The predicate "is a terminal category". A terminal category is a thin category with exactly one object. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ ∃!𝑥 𝑥 ∈ 𝐵))
Theorem	istermc3 49223	The predicate "is a terminal category". A terminal category is a thin category whose base set is equinumerous to 1o. Consider en1b 9034, map1 9049, and euen1b 9037. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ 𝐵 ≈ 1o))
Theorem	termcthin 49224	A terminal category is a thin category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝐶 ∈ TermCat → 𝐶 ∈ ThinCat)
Theorem	termcthind 49225	A terminal category is a thin category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	termccd 49226	A terminal category is a category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	termcbas 49227*	The base of a terminal category is a singleton. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∃𝑥 𝐵 = {𝑥})
Theorem	termcbas2 49228	The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = {𝑋})
Theorem	termcbasmo 49229	Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	termchomn0 49230	All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅)
Theorem	termchommo 49231	All morphisms of a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	termcid 49232	The morphism of a terminal category is an identity morphism. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑋))
Theorem	termcid2 49233	The morphism of a terminal category is an identity morphism. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑌))
Theorem	termchom 49234	The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = {( 1 ‘𝑋)})
Theorem	termchom2 49235	The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = {( 1 ‘𝑍)})
Theorem	setcsnterm 49236	The category of one set, either a singleton set or an empty set, is terminal. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ (SetCat‘{{𝐴}}) ∈ TermCat
Theorem	setc1oterm 49237	The category (SetCat‘1o), i.e., the trivial category, is terminal. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ (SetCat‘1o) ∈ TermCat
Theorem	setc1obas 49238	The base of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ 1o = (Base‘ 1 )
Theorem	setc1ohomfval 49239	Set of morphisms of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ {⟨∅, ∅, 1o⟩} = (Hom ‘ 1 )
Theorem	setc1ocofval 49240	Composition in the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ {⟨⟨∅, ∅⟩, ∅, {⟨∅, ∅, ∅⟩}⟩} = (comp‘ 1 )
Theorem	setc1oid 49241	The identity morphism of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐼 = (Id‘ 1 )    ⇒   ⊢ (𝐼‘∅) = ∅
Theorem	funcsetc1ocl 49242	The functor to the trivial category. The converse is also true due to reverse closure. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 1 ))
Theorem	funcsetc1o 49243*	Value of the functor to the trivial category. The converse is also true because 𝐹 would be the empty set if 𝐶 were not a category; and the empty set cannot equal an ordered pair of two sets. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐹 = ⟨(𝐵 × 1o), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × 1o))⟩)
Theorem	isinito2lem 49244	The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼(𝐹(𝐶UP 1 )∅)∅))
Theorem	isinito2 49245	The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅)    ⇒   ⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼(𝐹(𝐶UP 1 )∅)∅)
Theorem	isinito3 49246	The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘∅)    ⇒   ⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ dom (𝐹(𝐶UP 1 )∅))
Theorem	dfinito4 49247*	An alternate definition of df-inito 17984 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 17984. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐UP𝑑)∅))
Theorem	dftermo4 49248*	An alternate definition of df-termo 17985 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 17985. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ TermO = (𝑐 ∈ Cat ↦ ⦋(oppCat‘𝑐) / 𝑜⦌⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑜))‘∅) / 𝑓⦌dom (𝑓(𝑜UP𝑑)∅))
Theorem	termcpropd 49249	Two structures with the same base, hom-sets and composition operation are either both terminal categories or neither. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐶 ∈ TermCat ↔ 𝐷 ∈ TermCat))
Theorem	oppctermhom 49250	The opposite category of a terminal category has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂))
Theorem	oppctermco 49251	The opposite category of a terminal category has the same base, hom-sets and composition operation as the original category. Note that 𝐶 = 𝑂 cannot be proved because 𝐶 might not even be a function. For example, let 𝐶 be ({⟨(Base‘ndx), {∅}⟩, ⟨(Hom ‘ndx), ((V × V) × {{∅}})⟩} ∪ {⟨(comp‘ndx), {∅}⟩, ⟨(comp‘ndx), 2o⟩}); it should be a terminal category, but the opposite category is not itself. See the definitions df-oppc 17711 and df-sets 17170. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcterm 49252	The opposite category of a terminal category is a terminal category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝑂 ∈ TermCat)
Theorem	functermclem 49253	Lemma for functermc 49254. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ ((𝜑 ∧ 𝐾𝑅𝐿) → 𝐾 = 𝐹)    &   ⊢ (𝜑 → (𝐹𝑅𝐿 ↔ 𝐿 = 𝐺))    ⇒   ⊢ (𝜑 → (𝐾𝑅𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺)))
Theorem	functermc 49254*	Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝐹 = (𝐵 × 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (𝐾(𝐷 Func 𝐸)𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺)))
Theorem	functermc2 49255*	Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝐹 = (𝐵 × 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝐹, 𝐺⟩})
Theorem	functermceu 49256*	There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷))
Theorem	fulltermc 49257*	A functor to a terminal category is full iff all hom-sets of the source category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ (𝑥𝐻𝑦) = ∅))
Theorem	fulltermc2 49258	Given a full functor to a terminal category, the source category must not have empty hom-sets. (Contributed by Zhi Wang, 17-Oct-2025.) (Proof shortened by Zhi Wang, 6-Nov-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅)
Theorem	termcterm 49259	A terminal category is a terminal object of the category of small categories. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (TermO‘𝐸))
Theorem	termcterm2 49260	A terminal object of the category of small categories is a terminal category. (Contributed by Zhi Wang, 18-Oct-2025.) (Proof shortened by Zhi Wang, 23-Oct-2025.)
⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → (𝑈 ∩ TermCat) ≠ ∅)    &   ⊢ (𝜑 → 𝐶 ∈ (TermO‘𝐸))    ⇒   ⊢ (𝜑 → 𝐶 ∈ TermCat)
Theorem	termcterm3 49261	In the category of small categories, a terminal object is equivalent to a terminal category. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → (SetCat‘1o) ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐶 ∈ TermCat ↔ 𝐶 ∈ (TermO‘𝐸)))
Theorem	termcciso 49262	A category is isomorphic to a terminal category iff it itself is terminal. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ TermCat)    ⇒   ⊢ (𝜑 → (𝑌 ∈ TermCat ↔ 𝑋( ≃𝑐 ‘𝐶)𝑌))
Theorem	termccisoeu 49263*	The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ TermCat)    &   ⊢ (𝜑 → 𝑌 ∈ TermCat)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝑋(Iso‘𝐶)𝑌))
Theorem	termc2 49264*	If there exists a unique functor from both the category itself and the trivial category, then the category is terminal. Note that the converse also holds, so that it is a biconditional. See the proof of termc 49265 for hints. See also eufunc 49268 and euendfunc2 49273 for some insights on why two categories are sufficient. (Contributed by Zhi Wang, 18-Oct-2025.) (Proof shortened by Zhi Wang, 20-Oct-2025.)
⊢ (∀𝑑 ∈ ({𝐶, (SetCat‘1o)} ∩ Cat)∃!𝑓 𝑓 ∈ (𝑑 Func 𝐶) → 𝐶 ∈ TermCat)
Theorem	termc 49265*	Alternate definition of TermCat. See also df-termc 49220. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ (𝐶 ∈ TermCat ↔ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝐶))
Theorem	dftermc2 49266*	Alternate definition of TermCat. See also df-termc 49220 and dftermc3 49277. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ TermCat = {𝑐 ∣ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝑐)}
Theorem	eufunclem 49267*	If there exists a unique functor from a non-empty category, then the base of the target category is at most a singleton. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ 𝐵 = (Base‘𝐷)    ⇒   ⊢ (𝜑 → 𝐵 ≼ 1o)
Theorem	eufunc 49268*	If there exists a unique functor from a non-empty category, then the base of the target category is a singleton. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ 𝐵 = (Base‘𝐷)    ⇒   ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵)
Theorem	idfudiag1lem 49269	Lemma for idfudiag1bas 49270 and idfudiag1 49271. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ (𝜑 → ( I ↾ 𝐴) = (𝐴 × {𝐵}))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐴 = {𝐵})
Theorem	idfudiag1bas 49270	If the identity functor of a category is the same as a constant functor to the category, then the base is a singleton. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐿 = (𝐶Δfunc𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ (𝜑 → 𝐼 = 𝐾)    ⇒   ⊢ (𝜑 → 𝐵 = {𝑋})
Theorem	idfudiag1 49271	If the identity functor of a category is the same as a constant functor to the category, then the category is terminal. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐿 = (𝐶Δfunc𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ (𝜑 → 𝐼 = 𝐾)    ⇒   ⊢ (𝜑 → 𝐶 ∈ TermCat)
Theorem	euendfunc 49272*	If there exists a unique endofunctor (a functor from a category to itself) for a non-empty category, then the category is terminal. This partially explains why two categories are sufficient in termc2 49264. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐶))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐶 ∈ TermCat)
Theorem	euendfunc2 49273	If there exists a unique endofunctor (a functor from a category to itself) for a category, then it is either initial (empty) or terminal. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ ((𝐶 Func 𝐶) ≈ 1o → ((Base‘𝐶) = ∅ ∨ 𝐶 ∈ TermCat))
Theorem	termcarweu 49274*	There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐶 ∈ TermCat → ∃!𝑎 𝑎 ∈ (Arrow‘𝐶))
Theorem	arweuthinc 49275*	If a structure has a unique disjointified arrow, then the structure is a thin category. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (∃!𝑎 𝑎 ∈ (Arrow‘𝐶) → 𝐶 ∈ ThinCat)
Theorem	arweutermc 49276*	If a structure has a unique disjointified arrow, then the structure is a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (∃!𝑎 𝑎 ∈ (Arrow‘𝐶) → 𝐶 ∈ TermCat)
Theorem	dftermc3 49277	Alternate definition of TermCat. See also df-termc 49220, dftermc2 49266. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat = {𝑐 ∣ (Arrow‘𝑐) ≈ 1o}
Theorem	termcfuncval 49278	The value of a functor from a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐶))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑋 = ((1st ‘𝐾)‘𝑌)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐷)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐴 ∧ 𝐾 = ⟨{⟨𝑌, 𝑋⟩}, {⟨⟨𝑌, 𝑌⟩, {⟨(𝐼‘𝑌), ( 1 ‘𝑋)⟩}⟩}⟩))
Theorem	diag1f1olem 49279	To any functor from a terminal category can an object in the target base be assigned. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐶))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑋 = ((1st ‘𝐾)‘𝑌)    &   ⊢ 𝐿 = (𝐶Δfunc𝐷)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐴 ∧ 𝐾 = ((1st ‘𝐿)‘𝑋)))
Theorem	diag1f1o 49280	The object part of the diagonal functor is a bijection if 𝐷 is terminal. So any functor from a terminal category is one-to-one correspondent to an object of the target base. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐿 = (𝐶Δfunc𝐷)    ⇒   ⊢ (𝜑 → (1st ‘𝐿):𝐴–1-1-onto→(𝐷 Func 𝐶))
Theorem	termcnatval 49281	Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑅 = (𝐴‘𝑋)    ⇒   ⊢ (𝜑 → 𝐴 = {⟨𝑋, 𝑅⟩})
Theorem	diag2f1olem 49282	Lemma for diag2f1o 49283. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝑀 ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌)))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑀‘𝑍)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑀 = ((𝑋(2nd ‘𝐿)𝑌)‘𝐹)))
Theorem	diag2f1o 49283	If 𝐷 is terminal, the morphism part of a diagonal functor is bijective functions from hom-sets into sets of natural transformations. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝐿)𝑌):(𝑋𝐻𝑌)–1-1-onto→(((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌)))
Theorem	diagffth 49284	The diagonal functor is a fully faithful functor from a category 𝐶 to the category of functors from a terminal category to 𝐶. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    &   ⊢ 𝐿 = (𝐶Δfunc𝐷)    ⇒   ⊢ (𝜑 → 𝐿 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
Theorem	diagciso 49285	The diagonal functor is an isomorphism from a category 𝐶 to the category of functors from a terminal category to 𝐶. It is provable that the inverse of the diagonal functor is the mapped object by the transposed curry of (𝐷 evalF 𝐶), i.e., ∪ ran (1st ‘(⟨𝐷, 𝑄⟩ curryF ((𝐷 evalF 𝐶) ∘func (𝐷swapF𝑄)))). (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    &   ⊢ 𝐼 = (Iso‘𝐸)    &   ⊢ 𝐿 = (𝐶Δfunc𝐷)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐶𝐼𝑄))
Theorem	diagcic 49286	Any category 𝐶 is isomorphic to the category of functors from a terminal category to 𝐶. See also the "Properties" section of https://ncatlab.org/nlab/show/terminal+category. Therefore the number of categories isomorphic to a non-empty category is at least the number of singletons, so large (snnex 7747) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐶( ≃𝑐 ‘𝐸)𝑄)
21.49.16.3  Preordered sets as thin categories
Syntax	cprstc 49287	Class function defining preordered sets as categories.
class ProsetToCat
Definition	df-prstc 49288	Definition of the function converting a preordered set to a category. Justified by prsthinc 49211. This definition is somewhat arbitrary. Example 3.3(4.d) of [Adamek] p. 24 demonstrates an alternate definition with pairwise disjoint hom-sets. The behavior of the function is defined entirely, up to isomorphism (thincciso 49202), by prstcnid 49291, prstchom 49300, and prstcthin 49299. Other important properties include prstcbas 49292, prstcleval 49293, prstcle 49294, prstcocval 49295, prstcoc 49296, prstchom2 49301, and prstcprs 49298. Use those instead. Note that the defining property prstchom 49300 is equivalent to prstchom2 49301 given prstcthin 49299. See thincn0eu 49180 for justification. "ProsetToCat" was taken instead of "ProsetCat" because the latter might mean the category of preordered sets (classes). However, "ProsetToCat" seems too long. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Theorem	prstcval 49289	Lemma for prstcnidlem 49290 and prstcthin 49299. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Theorem	prstcnidlem 49290	Lemma for prstcnid 49291 and prstchomval 49297. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (comp‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝐶) = (𝐸‘(𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩)))
Theorem	prstcnid 49291	Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (comp‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Hom ‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝐾) = (𝐸‘𝐶))
Theorem	prstcbas 49292	The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	prstcleval 49293	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → ≤ = (le‘𝐶))
Theorem	prstcle 49294	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌))
Theorem	prstcocval 49295	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ⊥ = (oc‘𝐶))
Theorem	prstcoc 49296	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋))
Theorem	prstchomval 49297	Hom-sets of the constructed category which depend on an arbitrary definition. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    ⇒   ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶))
Theorem	prstcprs 49298	The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	prstcthin 49299	The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	prstchom 49300	Hom-sets of the constructed category are dependent on the preorder. Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat. However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))