P. 495 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49401-49500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isthinc 49401*	The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)))
Theorem	isthinc2 49402*	A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ≼ 1o))
Theorem	isthinc3 49403*	A thin category is a category in which, given a pair of objects 𝑥 and 𝑦 and any two morphisms 𝑓, 𝑔 from 𝑥 to 𝑦, the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑥𝐻𝑦)𝑓 = 𝑔))
Theorem	thincc 49404	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝐶 ∈ ThinCat → 𝐶 ∈ Cat)
Theorem	thinccd 49405	A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	thincssc 49406	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ThinCat ⊆ Cat
Theorem	isthincd2lem1 49407*	Lemma for isthincd2 49419 and thincmo2 49408. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thincmo2 49408	Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thinchom 49409	A non-empty hom-set of a thin category is given by its element. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = {𝐹})
Theorem	thincmo 49410*	There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmoALT 49411*	Alternate proof of thincmo 49410. (Contributed by Zhi Wang, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmod 49412*	At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincn0eu 49413*	In a thin category, a hom-set being non-empty is equivalent to having a unique element. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → ((𝑋𝐻𝑌) ≠ ∅ ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌)))
Theorem	thincid 49414	In a thin category, a morphism from an object to itself is an identity morphism. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑋))    ⇒   ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑋))
Theorem	thincmon 49415	In a thin category, all morphisms are monomorphisms. Example 7.33(9) of [Adamek] p. 110. The converse does not hold. See grptcmon 49575. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌))
Theorem	thincepi 49416	In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi 49576. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Epi‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌))
Theorem	isthincd2lem2 49417*	Lemma for isthincd2 49419. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Theorem	isthincd 49418*	The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	isthincd2 49419*	The predicate "𝐶 is a thin category" without knowing 𝐶 is a category (deduction form). The identity arrow operator is also provided as a byproduct. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )))
Theorem	oppcthin 49420	The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat)
Theorem	oppcthinco 49421	If the opposite category of a thin category has the same base and hom-sets as the original category, then it has the same composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcthinendc 49422*	The opposite category of a thin category whose morphisms are all endomorphisms has the same base, hom-sets (oppcendc 49000) and composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcthinendcALT 49423*	Alternate proof of oppcthinendc 49422. (Contributed by Zhi Wang, 16-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	thincpropd 49424	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 49425	A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ThinCat)
Theorem	functhinclem1 49426*	Lemma for functhinc 49430. 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 49427*	Lemma for functhinc 49430. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))
Theorem	functhinclem3 49428*	Lemma for functhinc 49430. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))))    &   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))    &   ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	functhinclem4 49429*	Lemma for functhinc 49430. 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 49430*	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 48994), and can be obtained from funcf2 17810, f002 48835, and ralrimivva 3178. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    ⇒   ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾))
Theorem	functhincfun 49431	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 49432*	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 49433	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 49434	A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
Theorem	thincciso 49435*	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 17161. (Contributed by Zhi Wang, 16-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆)))
Theorem	thinccisod 49436*	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 49437	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 17161. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ThinCat)
Theorem	thincciso3 49438	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 17161. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑌 ∈ ThinCat)
Theorem	thincciso4 49439	Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv 17161. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat))
Theorem	0thincg 49440	Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat)
Theorem	0thinc 49441	The empty category (see 0cat 17630) is thin. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ∅ ∈ ThinCat
Theorem	indcthing 49442*	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 49443*	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 49444*	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 49446, 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 49445*	An alternate proof of indthinc 49444 assuming more axioms including ax-pow 5315 and ax-un 7691. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	prsthinc 49446*	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 48993 and catprs2 48994 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 49447*	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 49448	The category (SetCat‘2o) is thin. A special case of setcthin 49447. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (SetCat‘2o) ∈ ThinCat
Theorem	thincsect 49449	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 49450	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 49451	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 49452	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 49453	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 49454	Extend class notation with the class of terminal categories.
class TermCat
Definition	df-termc 49455*	Definition of the proper class (termcnex 49558) 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 49468). 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 49497). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 49502). See also dftermc3 49513 where TermCat is defined as categories with exactly one disjointified arrow. Unlike https://ncatlab.org/nlab/show/terminal+category 49513, we reserve the term "trivial category" for (SetCat‘1o), justified by setc1oterm 49473. Followed directly from the definition, terminal categories are thin (termcthin 49459). The opposite category of a terminal category is "almost" itself (oppctermco 49487). Any category 𝐶 is isomorphic to the category of functors from a terminal category to the category 𝐶 (diagcic 49522). Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 49483) and terminal objects (dftermo4 49484). The universal properties provide an alternate proof of initoeu1 17953, termoeu1 17960, initoeu2 17958, and termoeu2 49220. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 49498). The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17629, 0thincg 49440, func0g 49071, 0funcg 49067, and initc 49073. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
Theorem	istermc 49456*	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 49457*	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 49458	The predicate "is a terminal category". A terminal category is a thin category whose base set is equinumerous to 1o. Consider en1b 8973, map1 8988, and euen1b 8976. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ 𝐵 ≈ 1o))
Theorem	termcthin 49459	A terminal category is a thin category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝐶 ∈ TermCat → 𝐶 ∈ ThinCat)
Theorem	termcthind 49460	A terminal category is a thin category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	termccd 49461	A terminal category is a category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	termcbas 49462*	The base of a terminal category is a singleton. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∃𝑥 𝐵 = {𝑥})
Theorem	termco 49463	The object of a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝐵 ∈ 𝐵)
Theorem	termcbas2 49464	The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = {𝑋})
Theorem	termcbasmo 49465	Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	termchomn0 49466	All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅)
Theorem	termchommo 49467	All morphisms of a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	termcid 49468	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 49469	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 49470	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 49471	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 49472	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 49473	The category (SetCat‘1o), i.e., the trivial category, is terminal. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ (SetCat‘1o) ∈ TermCat
Theorem	setc1obas 49474	The base of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ 1o = (Base‘ 1 )
Theorem	setc1ohomfval 49475	Set of morphisms of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ {⟨∅, ∅, 1o⟩} = (Hom ‘ 1 )
Theorem	setc1ocofval 49476	Composition in the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ {⟨⟨∅, ∅⟩, ∅, {⟨∅, ∅, ∅⟩}⟩} = (comp‘ 1 )
Theorem	setc1oid 49477	The identity morphism of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐼 = (Id‘ 1 )    ⇒   ⊢ (𝐼‘∅) = ∅
Theorem	funcsetc1ocl 49478	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 49479*	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 49480	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 49481	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 49482	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 49483*	An alternate definition of df-inito 17926 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 17926. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))
Theorem	dftermo4 49484*	An alternate definition of df-termo 17927 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 17927. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ TermO = (𝑐 ∈ Cat ↦ ⦋(oppCat‘𝑐) / 𝑜⦌⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑜))‘∅) / 𝑓⦌dom (𝑓(𝑜 UP 𝑑)∅))
Theorem	termcpropd 49485	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 49486	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 49487	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 17653 and df-sets 17110. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcterm 49488	The opposite category of a terminal category is a terminal category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝑂 ∈ TermCat)
Theorem	functermclem 49489	Lemma for functermc 49490. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ ((𝜑 ∧ 𝐾𝑅𝐿) → 𝐾 = 𝐹)    &   ⊢ (𝜑 → (𝐹𝑅𝐿 ↔ 𝐿 = 𝐺))    ⇒   ⊢ (𝜑 → (𝐾𝑅𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺)))
Theorem	functermc 49490*	Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝐹 = (𝐵 × 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (𝐾(𝐷 Func 𝐸)𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺)))
Theorem	functermc2 49491*	Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝐹 = (𝐵 × 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝐹, 𝐺⟩})
Theorem	functermceu 49492*	There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷))
Theorem	fulltermc 49493*	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 49494	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 49495	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 49496	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 49497	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 49498	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 49499*	The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ TermCat)    &   ⊢ (𝜑 → 𝑌 ∈ TermCat)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝑋(Iso‘𝐶)𝑌))
Theorem	termc2 49500*	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 49501 for hints. See also eufunc 49504 and euendfunc2 49509 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)