P. 496 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49501-49600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eufunc 49501*	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 49502	Lemma for idfudiag1bas 49503 and idfudiag1 49504. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ (𝜑 → ( I ↾ 𝐴) = (𝐴 × {𝐵}))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐴 = {𝐵})
Theorem	idfudiag1bas 49503	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 49504	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 49505*	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 49497. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐶))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐶 ∈ TermCat)
Theorem	euendfunc2 49506	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 49507*	There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐶 ∈ TermCat → ∃!𝑎 𝑎 ∈ (Arrow‘𝐶))
Theorem	arweuthinc 49508*	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 49509*	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 49510	Alternate definition of TermCat. See also df-termc 49452, dftermc2 49499. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat = {𝑐 ∣ (Arrow‘𝑐) ≈ 1o}
Theorem	termcfuncval 49511	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 49512	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 49513	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 49514	Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑅 = (𝐴‘𝑋)    ⇒   ⊢ (𝜑 → 𝐴 = {⟨𝑋, 𝑅⟩})
Theorem	diag2f1olem 49515	Lemma for diag2f1o 49516. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝑀 ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌)))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑀‘𝑍)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑀 = ((𝑋(2nd ‘𝐿)𝑌)‘𝐹)))
Theorem	diag2f1o 49516	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 49517	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 49518	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 49519	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 7736) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐶( ≃𝑐 ‘𝐸)𝑄)
Theorem	funcsn 49520	The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐶 Func 𝐷) = {𝐹})    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)
Theorem	fucterm 49521	The category of functors to a terminal category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)
Theorem	0fucterm 49522	The category of functors from an initial category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)
Theorem	termfucterm 49523	All functors between two terminal categories are isomorphisms. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ TermCat)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ TermCat)    ⇒   ⊢ (𝜑 → (𝑋 Func 𝑌) = (𝑋𝐼𝑌))
Theorem	cofuterm 49524	Post-compose with a functor to a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐾 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾)
Theorem	uobeqterm 49525	Universal objects and terminal categories. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐴 = (Base‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    ⇒   ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌))
Theorem	isinito4 49526	The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 1 ∈ TermCat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘ 1 ))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 1 ))    ⇒   ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ dom (𝐹(𝐶 UP 1 )𝑋)))
Theorem	isinito4a 49527	The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 1 ∈ TermCat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘ 1 ))    &   ⊢ 𝐹 = ((1st ‘( 1 Δfunc𝐶))‘𝑋)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ dom (𝐹(𝐶 UP 1 )𝑋)))
21.49.16.4  Preordered sets as thin categories
Syntax	cprstc 49528	Class function defining preordered sets as categories.
class ProsetToCat
Definition	df-prstc 49529	Definition of the function converting a preordered set to a category. Justified by prsthinc 49443. This definition is somewhat arbitrary. Example 3.3(4.d) of [Adamek] p. 24 demonstrates an alternate definition with pairwise disjoint hom-sets. The behavior of the function is defined entirely, up to isomorphism (thincciso 49432), by prstcnid 49532, prstchom 49541, and prstcthin 49540. Other important properties include prstcbas 49533, prstcleval 49534, prstcle 49535, prstcocval 49536, prstcoc 49537, prstchom2 49542, and prstcprs 49539. Use those instead. Note that the defining property prstchom 49541 is equivalent to prstchom2 49542 given prstcthin 49540. See thincn0eu 49410 for justification. "ProsetToCat" was taken instead of "ProsetCat" because the latter might mean the category of preordered sets (classes). However, "ProsetToCat" seems too long. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Theorem	prstcval 49530	Lemma for prstcnidlem 49531 and prstcthin 49540. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Theorem	prstcnidlem 49531	Lemma for prstcnid 49532 and prstchomval 49538. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (comp‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝐶) = (𝐸‘(𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩)))
Theorem	prstcnid 49532	Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (comp‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Hom ‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝐾) = (𝐸‘𝐶))
Theorem	prstcbas 49533	The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	prstcleval 49534	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → ≤ = (le‘𝐶))
Theorem	prstcle 49535	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌))
Theorem	prstcocval 49536	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ⊥ = (oc‘𝐶))
Theorem	prstcoc 49537	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋))
Theorem	prstchomval 49538	Hom-sets of the constructed category which depend on an arbitrary definition. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    ⇒   ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶))
Theorem	prstcprs 49539	The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	prstcthin 49540	The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	prstchom 49541	Hom-sets of the constructed category are dependent on the preorder. Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat. However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))
Theorem	prstchom2 49542*	Hom-sets of the constructed category are dependent on the preorder. Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat ( see prstchom2ALT 49543). However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌)))
Theorem	prstchom2ALT 49543*	Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 49529. See prstchom2 49542 for a version that does not depend on the definition. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌)))
Theorem	oduoppcbas 49544	The dual of a preordered set and the opposite category have the same set of objects. (Contributed by Zhi Wang, 22-Sep-2025.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → 𝐷 = (ProsetToCat‘(ODual‘𝐾)))    &   ⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝜑 → (Base‘𝐷) = (Base‘𝑂))
Theorem	oduoppcciso 49545	The dual of a preordered set and the opposite category are category-isomorphic. Example 3.6(1) of [Adamek] p. 25. (Contributed by Zhi Wang, 22-Sep-2025.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → 𝐷 = (ProsetToCat‘(ODual‘𝐾)))    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐷( ≃𝑐 ‘(CatCat‘𝑈))𝑂)
Theorem	postcpos 49546	The converted category is a poset iff the original proset is a poset. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset))
Theorem	postcposALT 49547	Alternate proof of postcpos 49546. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset))
Theorem	postc 49548*	The converted category is a poset iff no distinct objects are isomorphic. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Poset ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥( ≃𝑐 ‘𝐶)𝑦 → 𝑥 = 𝑦)))
Theorem	discsntermlem 49549*	A singlegon is an element of the class of singlegons. The converse (basrestermcfolem 49550) also holds. This is trivial if 𝐵 is 𝑏 (abid 2712). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (∃𝑥 𝐵 = {𝑥} → 𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}})
Theorem	basrestermcfolem 49550*	An element of the class of singlegons is a singlegon. The converse (discsntermlem 49549) also holds. This is trivial if 𝐵 is 𝑏 (abid 2712). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} → ∃𝑥 𝐵 = {𝑥})
Theorem	discbas 49551	A discrete category (a category whose only morphisms are the identity morphisms) can be constructed for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩}    &   ⊢ 𝐶 = (ProsetToCat‘𝐾)    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐶))
Theorem	discthin 49552	A discrete category (a category whose only morphisms are the identity morphisms) is thin. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩}    &   ⊢ 𝐶 = (ProsetToCat‘𝐾)    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐶 ∈ ThinCat)
Theorem	discsnterm 49553*	A discrete category (a category whose only morphisms are the identity morphisms) with a singlegon base is terminal. Corollary of example 3.3(4)(c) of [Adamek] p. 24 and example 3.26(1) of [Adamek] p. 33. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩}    &   ⊢ 𝐶 = (ProsetToCat‘𝐾)    ⇒   ⊢ (∃𝑥 𝐵 = {𝑥} → 𝐶 ∈ TermCat)
Theorem	basrestermcfo 49554*	The base function restricted to the class of terminal categories maps the class of terminal categories onto the class of singletons. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (Base ↾ TermCat):TermCat–onto→{𝑏 ∣ ∃𝑥 𝑏 = {𝑥}}
Theorem	termcnex 49555	The class of all terminal categories is a proper class. Therefore both the class of all thin categories and the class of all categories are proper classes. Note that snnex 7736 is equivalent to sngl V ∉ V. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat ∉ V
21.49.16.5  Monoids as categories
Syntax	cmndtc 49556	Class function defining monoids as categories.
class MndToCat
Definition	df-mndtc 49557	Definition of the function converting a monoid to a category. Example 3.3(4.e) of [Adamek] p. 24. The definition of the base set is arbitrary. The whole extensible structure becomes the object here (see mndtcbasval 49559), instead of just the base set, as is the case in Example 3.3(4.e) of [Adamek] p. 24. The resulting category is defined entirely, up to isomorphism, by mndtcbas 49560, mndtchom 49563, mndtcco 49564. Use those instead. See example 3.26(3) of [Adamek] p. 33 for more on isomorphism. "MndToCat" was taken instead of "MndCat" because the latter might mean the category of monoids. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})
Theorem	mndtcval 49558	Value of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), {𝑀}⟩, ⟨(Hom ‘ndx), {⟨𝑀, 𝑀, (Base‘𝑀)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g‘𝑀)⟩}⟩})
Theorem	mndtcbasval 49559	The base set of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = {𝑀})
Theorem	mndtcbas 49560*	The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵)
Theorem	mndtcob 49561	Lemma for mndtchom 49563 and mndtcco 49564. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑀)
Theorem	mndtcbas2 49562	Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	mndtchom 49563	The only hom-set of the category built from a monoid is the base set of the monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (Proof shortened by Zhi Wang, 22-Oct-2025.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (Base‘𝑀))
Theorem	mndtcco 49564	The composition of the category built from a monoid is the monoid operation. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → · = (comp‘𝐶))    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ · 𝑍) = (+g‘𝑀))
Theorem	mndtcco2 49565	The composition of the category built from a monoid is the monoid operation. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → ⚬ = (⟨𝑋, 𝑌⟩ · 𝑍))    ⇒   ⊢ (𝜑 → (𝐺 ⚬ 𝐹) = (𝐺(+g‘𝑀)𝐹))
Theorem	mndtccatid 49566*	Lemma for mndtccat 49567 and mndtcid 49568. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0g‘𝑀))))
Theorem	mndtccat 49567	The function value is a category. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	mndtcid 49568	The identity morphism, or identity arrow, of the category built from a monoid is the identity element of the monoid. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 1 = (Id‘𝐶))    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = (0g‘𝑀))
Theorem	oppgoppchom 49569	The converted opposite monoid has the same hom-set as that of the opposite category. Example 3.6(2) of [Adamek] p. 25. (Contributed by Zhi Wang, 21-Sep-2025.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐷 = (MndToCat‘(oppg‘𝑀)))    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑂))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐷))    &   ⊢ (𝜑 → 𝐽 = (Hom ‘𝑂))    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑋) = (𝑌𝐽𝑌))
Theorem	oppgoppcco 49570	The converted opposite monoid has the same composition as that of the opposite category. Example 3.6(2) of [Adamek] p. 25. (Contributed by Zhi Wang, 22-Sep-2025.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐷 = (MndToCat‘(oppg‘𝑀)))    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑂))    &   ⊢ (𝜑 → · = (comp‘𝐷))    &   ⊢ (𝜑 → ∙ = (comp‘𝑂))    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (⟨𝑌, 𝑌⟩ ∙ 𝑌))
Theorem	oppgoppcid 49571	The converted opposite monoid has the same identity morphism as that of the opposite category. Example 3.6(2) of [Adamek] p. 25. (Contributed by Zhi Wang, 22-Sep-2025.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐷 = (MndToCat‘(oppg‘𝑀)))    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑂))    ⇒   ⊢ (𝜑 → ((Id‘𝐷)‘𝑋) = ((Id‘𝑂)‘𝑌))
Theorem	grptcmon 49572	All morphisms in a category converted from a group are monomorphisms. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝑀 = (Mono‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌))
Theorem	grptcepi 49573	All morphisms in a category converted from a group are epimorphisms. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐸 = (Epi‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌))
21.49.16.6  Categories with at most one object and at most two morphisms
Theorem	2arwcatlem1 49574	Lemma for 2arwcat 49579. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝑋𝐻𝑋) = { 0 , 1 }    ⇒   ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
Theorem	2arwcatlem2 49575	Lemma for 2arwcat 49579. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) = 0 )    ⇒   ⊢ (𝜑 → ( 1 (⟨𝐴, 𝐵⟩ · 𝐶)𝐹) = 𝐹)
Theorem	2arwcatlem3 49576	Lemma for 2arwcat 49579. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 0 )    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐴, 𝐵⟩ · 𝐶) 1 ) = 𝐹)
Theorem	2arwcatlem4 49577	Lemma for 2arwcat 49579. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 0 )    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) = 0 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) ∈ { 0 , 1 })    &   ⊢ (𝜑 → (𝐺 = 0 ∨ 𝐺 = 1 ))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝐴, 𝐵⟩ · 𝐶)𝐹) ∈ { 0 , 1 })
Theorem	2arwcatlem5 49578	Lemma for 2arwcat 49579. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → ( 1 · 0 ) = 0 )    &   ⊢ (𝜑 → ( 0 · 1 ) = 0 )    &   ⊢ (𝜑 → ( 0 · 0 ) ∈ { 0 , 1 })    ⇒   ⊢ (𝜑 → (( 0 · 0 ) · 0 ) = ( 0 · ( 0 · 0 )))
Theorem	2arwcat 49579*	The condition for a structure with at most one object and at most two morphisms being a category. "2arwcat.2" to "2arwcat.5" are also necessary conditions if 𝑋, 0, and 1 are all sets, due to catlid 17650, catrid 17651, and catcocl 17652. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → {𝑋} = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝑋𝐻𝑋) = { 0 , 1 }    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑋⟩ · 𝑋) 1 ) = 1 )    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑋⟩ · 𝑋) 0 ) = 0 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑋⟩ · 𝑋) 1 ) = 0 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑋⟩ · 𝑋) 0 ) ∈ { 0 , 1 })    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ {𝑋} ↦ 1 )))
Theorem	incat 49580*	Constructing a category with at most one object and at most two morphisms. If 𝑋 is a set then 𝐶 is the category 𝐴 in Exercise 3G of [Adamek] p. 45. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝐶 = {⟨(Base‘ndx), {𝑋}⟩, ⟨(Hom ‘ndx), {⟨𝑋, 𝑋, 𝐻⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑋, 𝑋⟩, 𝑋, · ⟩}⟩}    &   ⊢ 𝐻 = {𝐹, 𝐺}    &   ⊢ · = (𝑓 ∈ 𝐻, 𝑔 ∈ 𝐻 ↦ (𝑓 ∩ 𝑔))    ⇒   ⊢ ((𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ {𝑋} ↦ 𝐺)))
Theorem	setc1onsubc 49581*	Construct a category with one object and two morphisms and prove that category (SetCat‘1o) satisfies all conditions for a subcategory but the compatibility of identity morphisms, showing the necessity of the latter condition in defining a subcategory. Exercise 4A of [Adamek] p. 58. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ 𝐶 = {⟨(Base‘ndx), {∅}⟩, ⟨(Hom ‘ndx), {⟨∅, ∅, 2o⟩}⟩, ⟨(comp‘ndx), {⟨⟨∅, ∅⟩, ∅, · ⟩}⟩}    &   ⊢ · = (𝑓 ∈ 2o, 𝑔 ∈ 2o ↦ (𝑓 ∩ 𝑔))    &   ⊢ 𝐸 = (SetCat‘1o)    &   ⊢ 𝐽 = (Homf ‘𝐸)    &   ⊢ 𝑆 = 1o    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝐷 = (𝐶 ↾cat 𝐽)    ⇒   ⊢ (𝐶 ∈ Cat ∧ 𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat 𝐻 ∧ ¬ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat))
Theorem	cnelsubclem 49582*	Lemma for cnelsubc 49583. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ 𝐽 ∈ V    &   ⊢ 𝑆 ∈ V    &   ⊢ (𝐶 ∈ Cat ∧ 𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ ¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))    ⇒   ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat))
Theorem	cnelsubc 49583*	Remark 4.2(2) of [Adamek] p. 48. There exists a category satisfying all conditions for a subcategory but the compatibility of identity morphisms. Therefore such condition in df-subc 17780 is necessary. A stronger statement than nelsubc3 49050. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat))
21.49.17  Kan extensions and related concepts
21.49.17.1  Kan extensions
Syntax	clan 49584	Class function defining the (local) left Kan extension.
class Lan
Syntax	cran 49585	Class function defining the (local) right Kan extension.
class Ran
Definition	df-lan 49586*	Definition of the (local) left Kan extension. Given a functor 𝐹:𝐶⟶𝐷 and a functor 𝑋:𝐶⟶𝐸, the set (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) consists of left Kan extensions of 𝑋 along 𝐹, which are universal pairs from 𝑋 to the pre-composition functor given by 𝐹 (lanval2 49606). See also § 3 of Chapter X in p. 240 of Mac Lane, Saunders, Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf 49606 (retrieved 3 Nov 2025). A left Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (lanrcl4 49613) and the second component is a natural transformation 𝐴:𝑋⟶𝐿𝐹 (lanrcl5 49614) where 𝐿𝐹 is the composed functor. Intuitively, the first component 𝐿 can be regarded as the result of an "inverse" of pre-composition; the source category of 𝑋:𝐶⟶𝐸 is "extended" along 𝐹:𝐶⟶𝐷. The left Kan extension is a generalization of many categorical concepts such as colimit. In § 7 of Chapter X of Categories for the Working Mathematician, it is concluded that "the notion of Kan extensions subsumes all the other fundamental concepts of category theory". This definition was chosen over the other version in the commented out section due to its better reverse closure property. See df-ran 49587 for the dual concept. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Lan = (𝑝 ∈ (V × V), 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ ((⟨𝑑, 𝑒⟩ −∘F 𝑓)((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))𝑥)))
Definition	df-ran 49587*	Definition of the (local) right Kan extension. Given a functor 𝐹:𝐶⟶𝐷 and a functor 𝑋:𝐶⟶𝐸, the set (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) consists of right Kan extensions of 𝑋 along 𝐹, which are universal pairs from the pre-composition functor given by 𝐹 to 𝑋 (ranval2 49609). The definition in § 3 of Chapter X in p. 236 of Mac Lane, Saunders, Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf 49609 (retrieved 3 Nov 2025). A right Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (ranrcl4 49618) and the second component is a natural transformation 𝐴:𝐿𝐹⟶𝑋 (ranrcl5 49619) where 𝐿𝐹 is the composed functor. Intuitively, the first component 𝐿 can be regarded as the result of an "inverse" of pre-composition; the source category of 𝑋:𝐶⟶𝐸 is "extended" along 𝐹:𝐶⟶𝐷. The right Kan extension is a generalization of many categorical concepts such as limit. In § 7 of Chapter X of Categories for the Working Mathematician, it is concluded that "the notion of Kan extensions subsumes all the other fundamental concepts of category theory". This definition was chosen over the other version in the commented out section due to its better reverse closure property. See df-lan 49586 for the dual concept. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Ran = (𝑝 ∈ (V × V), 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ (( oppFunc ‘(⟨𝑑, 𝑒⟩ −∘F 𝑓))((oppCat‘(𝑑 FuncCat 𝑒)) UP (oppCat‘(𝑐 FuncCat 𝑒)))𝑥)))
Theorem	lanfn 49588	Lan is a function on ((V × V) × V). (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Lan Fn ((V × V) × V)
Theorem	ranfn 49589	Ran is a function on ((V × V) × V). (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Ran Fn ((V × V) × V)
Theorem	reldmlan 49590	The domain of Lan is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom Lan
Theorem	reldmran 49591	The domain of Ran is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom Ran
Theorem	lanfval 49592*	Value of the function generating the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ Lan 𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (𝐶 Func 𝐸) ↦ ((⟨𝐷, 𝐸⟩ −∘F 𝑓)(𝑅 UP 𝑆)𝑥)))
Theorem	ranfval 49593*	Value of the function generating the set of right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ 𝑂 = (oppCat‘𝑅)    &   ⊢ 𝑃 = (oppCat‘𝑆)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ Ran 𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (𝐶 Func 𝐸) ↦ (( oppFunc ‘(⟨𝐷, 𝐸⟩ −∘F 𝑓))(𝑂 UP 𝑃)𝑥)))
Theorem	lanpropd 49594	If the categories have the same set of objects, morphisms, and compositions, then they have the same left Kan extensions. (Contributed by Zhi Wang, 21-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → (Homf ‘𝐸) = (Homf ‘𝐹))    &   ⊢ (𝜑 → (compf‘𝐸) = (compf‘𝐹))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐶⟩ Lan 𝐸) = (⟨𝐵, 𝐷⟩ Lan 𝐹))
Theorem	ranpropd 49595	If the categories have the same set of objects, morphisms, and compositions, then they have the same right Kan extensions. (Contributed by Zhi Wang, 21-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → (Homf ‘𝐸) = (Homf ‘𝐹))    &   ⊢ (𝜑 → (compf‘𝐸) = (compf‘𝐹))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐶⟩ Ran 𝐸) = (⟨𝐵, 𝐷⟩ Ran 𝐹))
Theorem	reldmlan2 49596	The domain of (𝑃 Lan 𝐸) is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom (𝑃 Lan 𝐸)
Theorem	reldmran2 49597	The domain of (𝑃 Ran 𝐸) is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom (𝑃 Ran 𝐸)
Theorem	lanval 49598	Value of the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = 𝐾)    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	ranval 49599	Value of the set of right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ 𝑂 = (oppCat‘𝑅)    &   ⊢ 𝑃 = (oppCat‘𝑆)    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) = (⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋))
Theorem	lanrcl 49600	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))