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	prcof2a 50001*	The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐾𝑃𝐿) = (𝑎 ∈ (𝐾𝑁𝐿) ↦ (𝑎 ∘ (1st ‘𝐹))))
Theorem	prcof2 50002*	The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩)) = 𝑃)    &   ⊢ Rel 𝑅    &   ⊢ (𝜑 → 𝐹𝑅𝐺)    ⇒   ⊢ (𝜑 → (𝐾𝑃𝐿) = (𝑎 ∈ (𝐾𝑁𝐿) ↦ (𝑎 ∘ 𝐹)))
Theorem	prcof21a 50003	The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾𝑁𝐿))    &   ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐾𝑃𝐿)‘𝐴) = (𝐴 ∘ (1st ‘𝐹)))
Theorem	prcof22a 50004	The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾𝑁𝐿))    &   ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (((𝐾𝑃𝐿)‘𝐴)‘𝑋) = (𝐴‘((1st ‘𝐹)‘𝑋)))
Theorem	prcofdiag1 50005	A constant functor pre-composed by a functor is another constant functor. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝑀 = (𝐶Δfunc𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((1st ‘𝐿)‘𝑋) ∘func 𝐹) = ((1st ‘𝑀)‘𝑋))
Theorem	prcofdiag 50006	A diagonal functor post-composed by a pre-composition functor is another diagonal functor. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝑀 = (𝐶Δfunc𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → (⟨𝐷, 𝐶⟩ −∘F 𝐹) = 𝐺)    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐿) = 𝑀)
21.49.16  Examples of categories
21.49.16.1  The category of categories
Theorem	catcrcl 50007	Reverse closure for the category of categories (in a universe) (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → 𝑈 ∈ V)
Theorem	catcrcl2 50008	Reverse closure for the category of categories (in a universe) (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
Theorem	elcatchom 50009	A morphism of the category of categories (in a universe) is a functor. See df-catc 18142 for the definition of the category Cat, which consists of all categories in the universe 𝑢 (i.e., "𝑢-small categories", see Definition 3.44. of [Adamek] p. 39), with functors as the morphisms (catchom 18146). (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑋 Func 𝑌))
Theorem	catcsect 50010	The property "𝐹 is a section of 𝐺 " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (idfunc‘𝑋)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝐹(𝑋𝑆𝑌)𝐺 ↔ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋)) ∧ (𝐺 ∘func 𝐹) = 𝐼))
Theorem	catcinv 50011	The property "𝐹 is an inverse of 𝐺 " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (idfunc‘𝑋)    &   ⊢ 𝐽 = (idfunc‘𝑌)    ⇒   ⊢ (𝐹(𝑋𝑁𝑌)𝐺 ↔ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋)) ∧ ((𝐺 ∘func 𝐹) = 𝐼 ∧ (𝐹 ∘func 𝐺) = 𝐽)))
Theorem	catcisoi 50012	A functor is an isomorphism of categories only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in [Adamek] p. 34. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆))
Theorem	uobeq2 50013	If a full functor (in fact, a full embedding) is a section, then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    &   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ 𝑄 = (CatCat‘𝑈)    &   ⊢ 𝑆 = (Sect‘𝑄)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Full 𝐸))    &   ⊢ (𝜑 → 𝐾 ∈ dom (𝐷𝑆𝐸))    ⇒   ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌))
Theorem	uobeq3 50014	An isomorphism between categories generates equal sets of universal objects. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    &   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ 𝑄 = (CatCat‘𝑈)    &   ⊢ 𝐼 = (Iso‘𝑄)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷𝐼𝐸))    ⇒   ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌))
Theorem	opf11 50015	The object part of the op functor on functor categories. Lemma for fucoppc 50022. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (1st ‘(𝐹‘𝑋)) = (1st ‘𝑋))
Theorem	opf12 50016	The object part of the op functor on functor categories. Lemma for oppfdiag 50028. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝑀(2nd ‘(𝐹‘𝑋))𝑁) = (𝑁(2nd ‘𝑋)𝑀))
Theorem	opf2fval 50017*	The morphism part of the op functor on functor categories. Lemma for fucoppc 50022. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑦𝑁𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = ( I ↾ (𝑌𝑁𝑋)))
Theorem	opf2 50018*	The morphism part of the op functor on functor categories. Lemma for fucoppc 50022. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑦𝑁𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (𝑌𝑁𝑋))    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌)‘𝐶) = 𝐷)
Theorem	fucoppclem 50019	Lemma for fucoppc 50022. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝑌𝑁𝑋) = ((𝐹‘𝑋)(𝑂 Nat 𝑃)(𝐹‘𝑌)))
Theorem	fucoppcid 50020*	The opposite category of functors is compatible with the category of opposite functors in terms of identity morphism. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (oppCat‘𝑄)    &   ⊢ 𝑆 = (𝑂 FuncCat 𝑃)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑋)‘((Id‘𝑅)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋)))
Theorem	fucoppcco 50021*	The opposite category of functors is compatible with the category of opposite functors in terms of composition. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (oppCat‘𝑄)    &   ⊢ 𝑆 = (𝑂 FuncCat 𝑃)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋(Hom ‘𝑅)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑌(Hom ‘𝑅)𝑍))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑍)‘(𝐵(⟨𝑋, 𝑌⟩(comp‘𝑅)𝑍)𝐴)) = (((𝑌𝐺𝑍)‘𝐵)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐴)))
Theorem	fucoppc 50022*	The isomorphism from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (oppCat‘𝑄)    &   ⊢ 𝑆 = (𝑂 FuncCat 𝑃)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥))))    &   ⊢ 𝑇 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐼 = (Iso‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹(𝑅𝐼𝑆)𝐺)
Theorem	fucoppcffth 50023*	A fully faithful functor from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (oppCat‘𝑄)    &   ⊢ 𝑆 = (𝑂 FuncCat 𝑃)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥))))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐹((𝑅 Full 𝑆) ∩ (𝑅 Faith 𝑆))𝐺)
Theorem	fucoppcfunc 50024*	A functor from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (oppCat‘𝑄)    &   ⊢ 𝑆 = (𝑂 FuncCat 𝑃)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐶 Func 𝐷), 𝑦 ∈ (𝐶 Func 𝐷) ↦ ( I ↾ (𝑦𝑁𝑥))))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	fucoppccic 50025	The opposite category of functors is isomorphic to the category of opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑋 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑌 = ((oppCat‘𝐷) FuncCat (oppCat‘𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)
Theorem	oppfdiag1 50026	A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐷 Func 𝐶)))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘((1st ‘𝐿)‘𝑋)) = ((1st ‘(𝑂Δfunc𝑃))‘𝑋))
Theorem	oppfdiag1a 50027	A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ( oppFunc ‘((1st ‘𝐿)‘𝑋)) = ((1st ‘(𝑂Δfunc𝑃))‘𝑋))
Theorem	oppfdiag 50028*	A diagonal functor for opposite categories is the opposite functor of the diagonal functor for original categories post-composed by an isomorphism (fucoppc 50022). (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 = ( oppFunc ↾ (𝐷 Func 𝐶)))    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ (𝜑 → 𝐺 = (𝑚 ∈ (𝐷 Func 𝐶), 𝑛 ∈ (𝐷 Func 𝐶) ↦ ( I ↾ (𝑛𝑁𝑚))))    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ∘func ( oppFunc ‘𝐿)) = (𝑂Δfunc𝑃))
21.49.16.2  Thin categories
Syntax	cthinc 50029	Extend class notation with the class of thin categories.
class ThinCat
Definition	df-thinc 50030*	Definition of the class of thin categories, or posetal categories, whose hom-sets each contain at most one morphism. Example 3.26(2) of [Adamek] p. 33. "ThinCat" was taken instead of "PosCat" because the latter might mean the category of posets. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ThinCat = {𝑐 ∈ Cat ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)}
Theorem	isthinc 50031*	The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)))
Theorem	isthinc2 50032*	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 50033*	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 50034	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝐶 ∈ ThinCat → 𝐶 ∈ Cat)
Theorem	thinccd 50035	A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	thincssc 50036	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ThinCat ⊆ Cat
Theorem	isthincd2lem1 50037*	Lemma for isthincd2 50049 and thincmo2 50038. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thincmo2 50038	Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thinchom 50039	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 50040*	There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmoALT 50041*	Alternate proof of thincmo 50040. (Contributed by Zhi Wang, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmod 50042*	At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincn0eu 50043*	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 50044	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 50045	In a thin category, all morphisms are monomorphisms. Example 7.33(9) of [Adamek] p. 110. The converse does not hold. See grptcmon 50205. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌))
Theorem	thincepi 50046	In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi 50206. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Epi‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌))
Theorem	isthincd2lem2 50047*	Lemma for isthincd2 50049. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Theorem	isthincd 50048*	The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	isthincd2 50049*	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 50050	The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat)
Theorem	oppcthinco 50051	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 50052*	The opposite category of a thin category whose morphisms are all endomorphisms has the same base, hom-sets (oppcendc 49630) and composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcthinendcALT 50053*	Alternate proof of oppcthinendc 50052. (Contributed by Zhi Wang, 16-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	thincpropd 50054	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 50055	A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ThinCat)
Theorem	functhinclem1 50056*	Lemma for functhinc 50060. 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 50057*	Lemma for functhinc 50060. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))
Theorem	functhinclem3 50058*	Lemma for functhinc 50060. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))))    &   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))    &   ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	functhinclem4 50059*	Lemma for functhinc 50060. 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 50060*	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 49624), and can be obtained from funcf2 17911, f002 49466, and ralrimivva 3206. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    ⇒   ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾))
Theorem	functhincfun 50061	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 50062*	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 50063	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 50064	A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
Theorem	thincciso 50065*	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 17261. (Contributed by Zhi Wang, 16-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆)))
Theorem	thinccisod 50066*	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 50067	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 17261. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ThinCat)
Theorem	thincciso3 50068	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 17261. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑌 ∈ ThinCat)
Theorem	thincciso4 50069	Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv 17261. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat))
Theorem	0thincg 50070	Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat)
Theorem	0thinc 50071	The empty category (see 0cat 17731) is thin. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ∅ ∈ ThinCat
Theorem	indcthing 50072*	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 50073*	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 50074*	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 50076, 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 50075*	An alternate proof of indthinc 50074 assuming more axioms including ax-pow 5323 and ax-un 7718. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	prsthinc 50076*	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 49623 and catprs2 49624 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 50077*	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 50078	The category (SetCat‘2o) is thin. A special case of setcthin 50077. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (SetCat‘2o) ∈ ThinCat
Theorem	thincsect 50079	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 50080	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 50081	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 50082	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 50083	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 50084	Extend class notation with the class of terminal categories.
class TermCat
Definition	df-termc 50085*	Definition of the proper class (termcnex 50188) 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 50098). 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 50127). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 50132). See also dftermc3 50143 where TermCat is defined as categories with exactly one disjointified arrow. Unlike https://ncatlab.org/nlab/show/terminal+category 50143, we reserve the term "trivial category" for (SetCat‘1o), justified by setc1oterm 50103. Followed directly from the definition, terminal categories are thin (termcthin 50089). The opposite category of a terminal category is "almost" itself (oppctermco 50117). Any category 𝐶 is isomorphic to the category of functors from a terminal category to the category 𝐶 (diagcic 50152). Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 50113) and terminal objects (dftermo4 50114). The universal properties provide an alternate proof of initoeu1 18054, termoeu1 18061, initoeu2 18059, and termoeu2 49850. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 50128). The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17730, 0thincg 50070, func0g 49701, 0funcg 49697, and initc 49703. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
Theorem	istermc 50086*	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 50087*	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 50088	The predicate "is a terminal category". A terminal category is a thin category whose base set is equinumerous to 1o. Consider en1b 9006, map1 9021, and euen1b 9009. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ 𝐵 ≈ 1o))
Theorem	termcthin 50089	A terminal category is a thin category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝐶 ∈ TermCat → 𝐶 ∈ ThinCat)
Theorem	termcthind 50090	A terminal category is a thin category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	termccd 50091	A terminal category is a category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	termcbas 50092*	The base of a terminal category is a singleton. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∃𝑥 𝐵 = {𝑥})
Theorem	termco 50093	The object of a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝐵 ∈ 𝐵)
Theorem	termcbas2 50094	The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = {𝑋})
Theorem	termcbasmo 50095	Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	termchomn0 50096	All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ¬ (𝑋𝐻𝑌) = ∅)
Theorem	termchommo 50097	All morphisms of a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	termcid 50098	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 50099	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 50100	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 ‘𝑋)})