P. 499 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49801-49900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	thincpropd 49801	Two structures with the same base, hom-sets and composition operation are either both thin categories or neither. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ↔ 𝐷 ∈ ThinCat))
Theorem	subthinc 49802	A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ThinCat)
Theorem	functhinclem1 49803*	Lemma for functhinc 49807. Given the object part, there is only one possible morphism part such that the mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    ⇒   ⊢ (𝜑 → ((𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝐺𝑤):(𝑧𝐻𝑤)⟶((𝐹‘𝑧)𝐽(𝐹‘𝑤))) ↔ 𝐺 = 𝐾))
Theorem	functhinclem2 49804*	Lemma for functhinc 49807. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))
Theorem	functhinclem3 49805*	Lemma for functhinc 49807. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))))    &   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))    &   ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	functhinclem4 49806*	Lemma for functhinc 49807. Other requirements on the morphism part are automatically satisfied. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ · = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝐸)    ⇒   ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))
Theorem	functhinc 49807*	A functor to a thin category is determined entirely by the object part. The hypothesis "functhinc.1" is related to a monotone function if preorders induced by the categories are considered (catprs2 49371), and can be obtained from funcf2 17804, f002 49213, and ralrimivva 3181. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    ⇒   ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾))
Theorem	functhincfun 49808	A functor to a thin category is determined entirely by the object part. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    ⇒   ⊢ (𝜑 → Fun (𝐶 Func 𝐷))
Theorem	fullthinc 49809*	A functor to a thin category is full iff empty hom-sets are mapped to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥𝐻𝑦) = ∅ → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅)))
Theorem	fullthinc2 49810	A full functor to a thin category maps empty hom-sets to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋𝐻𝑌) = ∅ ↔ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅))
Theorem	thincfth 49811	A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
Theorem	thincciso 49812*	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 17154. (Contributed by Zhi Wang, 16-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆)))
Theorem	thinccisod 49813*	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 49814	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 17154. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ThinCat)
Theorem	thincciso3 49815	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 17154. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑌 ∈ ThinCat)
Theorem	thincciso4 49816	Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv 17154. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat))
Theorem	0thincg 49817	Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat)
Theorem	0thinc 49818	The empty category (see 0cat 17624) is thin. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ∅ ∈ ThinCat
Theorem	indcthing 49819*	An indiscrete category, i.e., a category where all hom-sets have exactly one morphism, is thin. (Contributed by Zhi Wang, 11-Nov-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐻𝑦) = {𝐹})    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	discthing 49820*	A discrete category, i.e., a category where all morphisms are identity morphisms, is thin. Example 3.26(1) of [Adamek] p. 33. (Contributed by Zhi Wang, 11-Nov-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐻𝑦) = if(𝑥 = 𝑦, {𝐼}, ∅))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	indthinc 49821*	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 49823, 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 49822*	An alternate proof of indthinc 49821 assuming more axioms including ax-pow 5312 and ax-un 7690. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	prsthinc 49823*	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 49370 and catprs2 49371 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 49824*	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 49825	The category (SetCat‘2o) is thin. A special case of setcthin 49824. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (SetCat‘2o) ∈ ThinCat
Theorem	thincsect 49826	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 49827	In a thin category, 𝐹 is a section of 𝐺 iff 𝐺 is a section of 𝐹. Example 7.25(4) of [Adamek] p. 108. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ 𝐺(𝑌𝑆𝑋)𝐹))
Theorem	thincinv 49828	In a thin category, 𝐹 is an inverse of 𝐺 iff 𝐹 is a section of 𝐺. Example 7.20(7) of [Adamek] p. 107. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐹(𝑋𝑆𝑌)𝐺))
Theorem	thinciso 49829	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 49830	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.3  Terminal categories
Syntax	ctermc 49831	Extend class notation with the class of terminal categories.
class TermCat
Definition	df-termc 49832*	Definition of the proper class (termcnex 49935) 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 49845). 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 49874). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 49879). See also dftermc3 49890 where TermCat is defined as categories with exactly one disjointified arrow. Unlike https://ncatlab.org/nlab/show/terminal+category 49890, we reserve the term "trivial category" for (SetCat‘1o), justified by setc1oterm 49850. Followed directly from the definition, terminal categories are thin (termcthin 49836). The opposite category of a terminal category is "almost" itself (oppctermco 49864). Any category 𝐶 is isomorphic to the category of functors from a terminal category to the category 𝐶 (diagcic 49899). Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 49860) and terminal objects (dftermo4 49861). The universal properties provide an alternate proof of initoeu1 17947, termoeu1 17954, initoeu2 17952, and termoeu2 49597. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 49875). The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17623, 0thincg 49817, func0g 49448, 0funcg 49444, and initc 49450. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
Theorem	istermc 49833*	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 49834*	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 49835	The predicate "is a terminal category". A terminal category is a thin category whose base set is equinumerous to 1o. Consider en1b 8974, map1 8989, and euen1b 8977. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ 𝐵 ≈ 1o))
Theorem	termcthin 49836	A terminal category is a thin category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝐶 ∈ TermCat → 𝐶 ∈ ThinCat)
Theorem	termcthind 49837	A terminal category is a thin category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	termccd 49838	A terminal category is a category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	termcbas 49839*	The base of a terminal category is a singleton. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∃𝑥 𝐵 = {𝑥})
Theorem	termco 49840	The object of a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝐵 ∈ 𝐵)
Theorem	termcbas2 49841	The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = {𝑋})
Theorem	termcbasmo 49842	Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	termchomn0 49843	All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅)
Theorem	termchommo 49844	All morphisms of a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	termcid 49845	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 49846	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 49847	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 49848	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 49849	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 49850	The category (SetCat‘1o), i.e., the trivial category, is terminal. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ (SetCat‘1o) ∈ TermCat
Theorem	setc1obas 49851	The base of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ 1o = (Base‘ 1 )
Theorem	setc1ohomfval 49852	Set of morphisms of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ {⟨∅, ∅, 1o⟩} = (Hom ‘ 1 )
Theorem	setc1ocofval 49853	Composition in the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ {⟨⟨∅, ∅⟩, ∅, {⟨∅, ∅, ∅⟩}⟩} = (comp‘ 1 )
Theorem	setc1oid 49854	The identity morphism of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐼 = (Id‘ 1 )    ⇒   ⊢ (𝐼‘∅) = ∅
Theorem	funcsetc1ocl 49855	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 49856*	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 49857	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 49858	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 49859	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 49860*	An alternate definition of df-inito 17920 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 17920. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))
Theorem	dftermo4 49861*	An alternate definition of df-termo 17921 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 17921. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ TermO = (𝑐 ∈ Cat ↦ ⦋(oppCat‘𝑐) / 𝑜⦌⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑜))‘∅) / 𝑓⦌dom (𝑓(𝑜 UP 𝑑)∅))
Theorem	termcpropd 49862	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 49863	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 49864	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 17647 and df-sets 17103. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcterm 49865	The opposite category of a terminal category is a terminal category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝑂 ∈ TermCat)
Theorem	functermclem 49866	Lemma for functermc 49867. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ ((𝜑 ∧ 𝐾𝑅𝐿) → 𝐾 = 𝐹)    &   ⊢ (𝜑 → (𝐹𝑅𝐿 ↔ 𝐿 = 𝐺))    ⇒   ⊢ (𝜑 → (𝐾𝑅𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺)))
Theorem	functermc 49867*	Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝐹 = (𝐵 × 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (𝐾(𝐷 Func 𝐸)𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺)))
Theorem	functermc2 49868*	Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝐹 = (𝐵 × 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝐹, 𝐺⟩})
Theorem	functermceu 49869*	There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷))
Theorem	fulltermc 49870*	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 49871	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 49872	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 49873	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 49874	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 49875	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 49876*	The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ TermCat)    &   ⊢ (𝜑 → 𝑌 ∈ TermCat)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝑋(Iso‘𝐶)𝑌))
Theorem	termc2 49877*	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 49878 for hints. See also eufunc 49881 and euendfunc2 49886 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 49878*	Alternate definition of TermCat. See also df-termc 49832. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ (𝐶 ∈ TermCat ↔ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝐶))
Theorem	dftermc2 49879*	Alternate definition of TermCat. See also df-termc 49832 and dftermc3 49890. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ TermCat = {𝑐 ∣ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝑐)}
Theorem	eufunclem 49880*	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 49881*	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 49882	Lemma for idfudiag1bas 49883 and idfudiag1 49884. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ (𝜑 → ( I ↾ 𝐴) = (𝐴 × {𝐵}))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐴 = {𝐵})
Theorem	idfudiag1bas 49883	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 49884	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 49885*	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 49877. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐶))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐶 ∈ TermCat)
Theorem	euendfunc2 49886	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 49887*	There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐶 ∈ TermCat → ∃!𝑎 𝑎 ∈ (Arrow‘𝐶))
Theorem	arweuthinc 49888*	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 49889*	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 49890	Alternate definition of TermCat. See also df-termc 49832, dftermc2 49879. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat = {𝑐 ∣ (Arrow‘𝑐) ≈ 1o}
Theorem	termcfuncval 49891	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 49892	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 49893	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 49894	Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑅 = (𝐴‘𝑋)    ⇒   ⊢ (𝜑 → 𝐴 = {⟨𝑋, 𝑅⟩})
Theorem	diag2f1olem 49895	Lemma for diag2f1o 49896. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝑀 ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌)))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑀‘𝑍)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑀 = ((𝑋(2nd ‘𝐿)𝑌)‘𝐹)))
Theorem	diag2f1o 49896	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 49897	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 49898	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 49899	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 7713) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐶( ≃𝑐 ‘𝐸)𝑄)
Theorem	funcsn 49900	The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐶 Func 𝐷) = {𝐹})    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)