P. 501 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50001-50100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	thincpropd 50001	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 50002	A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ThinCat)
Theorem	functhinclem1 50003*	Lemma for functhinc 50007. 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 50004*	Lemma for functhinc 50007. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))
Theorem	functhinclem3 50005*	Lemma for functhinc 50007. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))))    &   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))    &   ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	functhinclem4 50006*	Lemma for functhinc 50007. 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 50007*	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 49571), and can be obtained from funcf2 17873, f002 49413, and ralrimivva 3195. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    ⇒   ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾))
Theorem	functhincfun 50008	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 50009*	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 50010	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 50011	A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
Theorem	thincciso 50012*	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 17223. (Contributed by Zhi Wang, 16-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆)))
Theorem	thinccisod 50013*	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 50014	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 17223. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ThinCat)
Theorem	thincciso3 50015	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 17223. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑌 ∈ ThinCat)
Theorem	thincciso4 50016	Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv 17223. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat))
Theorem	0thincg 50017	Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat)
Theorem	0thinc 50018	The empty category (see 0cat 17693) is thin. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ∅ ∈ ThinCat
Theorem	indcthing 50019*	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 50020*	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 50021*	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 50023, 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 50022*	An alternate proof of indthinc 50021 assuming more axioms including ax-pow 5312 and ax-un 7703. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	prsthinc 50023*	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 49570 and catprs2 49571 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 50024*	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 50025	The category (SetCat‘2o) is thin. A special case of setcthin 50024. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (SetCat‘2o) ∈ ThinCat
Theorem	thincsect 50026	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 50027	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 50028	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 50029	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 50030	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 50031	Extend class notation with the class of terminal categories.
class TermCat
Definition	df-termc 50032*	Definition of the proper class (termcnex 50135) 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 50045). 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 50074). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 50079). See also dftermc3 50090 where TermCat is defined as categories with exactly one disjointified arrow. Unlike https://ncatlab.org/nlab/show/terminal+category 50090, we reserve the term "trivial category" for (SetCat‘1o), justified by setc1oterm 50050. Followed directly from the definition, terminal categories are thin (termcthin 50036). The opposite category of a terminal category is "almost" itself (oppctermco 50064). Any category 𝐶 is isomorphic to the category of functors from a terminal category to the category 𝐶 (diagcic 50099). Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 50060) and terminal objects (dftermo4 50061). The universal properties provide an alternate proof of initoeu1 18016, termoeu1 18023, initoeu2 18021, and termoeu2 49797. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 50075). The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17692, 0thincg 50017, func0g 49648, 0funcg 49644, and initc 49650. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
Theorem	istermc 50033*	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 50034*	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 50035	The predicate "is a terminal category". A terminal category is a thin category whose base set is equinumerous to 1o. Consider en1b 8991, map1 9006, and euen1b 8994. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ 𝐵 ≈ 1o))
Theorem	termcthin 50036	A terminal category is a thin category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝐶 ∈ TermCat → 𝐶 ∈ ThinCat)
Theorem	termcthind 50037	A terminal category is a thin category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	termccd 50038	A terminal category is a category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	termcbas 50039*	The base of a terminal category is a singleton. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∃𝑥 𝐵 = {𝑥})
Theorem	termco 50040	The object of a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝐵 ∈ 𝐵)
Theorem	termcbas2 50041	The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = {𝑋})
Theorem	termcbasmo 50042	Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	termchomn0 50043	All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅)
Theorem	termchommo 50044	All morphisms of a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	termcid 50045	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 50046	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 50047	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 50048	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 50049	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 50050	The category (SetCat‘1o), i.e., the trivial category, is terminal. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ (SetCat‘1o) ∈ TermCat
Theorem	setc1obas 50051	The base of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ 1o = (Base‘ 1 )
Theorem	setc1ohomfval 50052	Set of morphisms of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ {⟨∅, ∅, 1o⟩} = (Hom ‘ 1 )
Theorem	setc1ocofval 50053	Composition in the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    ⇒   ⊢ {⟨⟨∅, ∅⟩, ∅, {⟨∅, ∅, ∅⟩}⟩} = (comp‘ 1 )
Theorem	setc1oid 50054	The identity morphism of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 1 = (SetCat‘1o)    &   ⊢ 𝐼 = (Id‘ 1 )    ⇒   ⊢ (𝐼‘∅) = ∅
Theorem	funcsetc1ocl 50055	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 50056*	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 50057	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 50058	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 50059	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 50060*	An alternate definition of df-inito 17989 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 17989. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))
Theorem	dftermo4 50061*	An alternate definition of df-termo 17990 using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects 17990. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ TermO = (𝑐 ∈ Cat ↦ ⦋(oppCat‘𝑐) / 𝑜⦌⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑜))‘∅) / 𝑓⦌dom (𝑓(𝑜 UP 𝑑)∅))
Theorem	termcpropd 50062	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 50063	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 50064	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 17716 and df-sets 17172. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcterm 50065	The opposite category of a terminal category is a terminal category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝑂 ∈ TermCat)
Theorem	functermclem 50066	Lemma for functermc 50067. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ ((𝜑 ∧ 𝐾𝑅𝐿) → 𝐾 = 𝐹)    &   ⊢ (𝜑 → (𝐹𝑅𝐿 ↔ 𝐿 = 𝐺))    ⇒   ⊢ (𝜑 → (𝐾𝑅𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺)))
Theorem	functermc 50067*	Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝐹 = (𝐵 × 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (𝐾(𝐷 Func 𝐸)𝐿 ↔ (𝐾 = 𝐹 ∧ 𝐿 = 𝐺)))
Theorem	functermc2 50068*	Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝐹 = (𝐵 × 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝐹, 𝐺⟩})
Theorem	functermceu 50069*	There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐷))
Theorem	fulltermc 50070*	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 50071	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 50072	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 50073	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 50074	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 50075	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 50076*	The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ TermCat)    &   ⊢ (𝜑 → 𝑌 ∈ TermCat)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝑋(Iso‘𝐶)𝑌))
Theorem	termc2 50077*	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 50078 for hints. See also eufunc 50081 and euendfunc2 50086 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 50078*	Alternate definition of TermCat. See also df-termc 50032. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ (𝐶 ∈ TermCat ↔ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝐶))
Theorem	dftermc2 50079*	Alternate definition of TermCat. See also df-termc 50032 and dftermc3 50090. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ TermCat = {𝑐 ∣ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝑑 Func 𝑐)}
Theorem	eufunclem 50080*	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 50081*	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 50082	Lemma for idfudiag1bas 50083 and idfudiag1 50084. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ (𝜑 → ( I ↾ 𝐴) = (𝐴 × {𝐵}))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐴 = {𝐵})
Theorem	idfudiag1bas 50083	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 50084	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 50085*	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 50077. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐶))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐶 ∈ TermCat)
Theorem	euendfunc2 50086	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 50087*	There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐶 ∈ TermCat → ∃!𝑎 𝑎 ∈ (Arrow‘𝐶))
Theorem	arweuthinc 50088*	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 50089*	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 50090	Alternate definition of TermCat. See also df-termc 50032, dftermc2 50079. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat = {𝑐 ∣ (Arrow‘𝑐) ≈ 1o}
Theorem	termcfuncval 50091	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 50092	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 50093	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 50094	Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑅 = (𝐴‘𝑋)    ⇒   ⊢ (𝜑 → 𝐴 = {⟨𝑋, 𝑅⟩})
Theorem	diag2f1olem 50095	Lemma for diag2f1o 50096. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝑀 ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌)))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑀‘𝑍)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑀 = ((𝑋(2nd ‘𝐿)𝑌)‘𝐹)))
Theorem	diag2f1o 50096	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 50097	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 50098	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 50099	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 7726) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐶( ≃𝑐 ‘𝐸)𝑄)
Theorem	funcsn 50100	The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐶 Func 𝐷) = {𝐹})    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)