P. 507 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50601-50700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	idfudiag1bas 50601	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 50602	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 50603*	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 50595. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐶 Func 𝐶))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → 𝐶 ∈ TermCat)
Theorem	euendfunc2 50604	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 50605*	There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐶 ∈ TermCat → ∃!𝑎 𝑎 ∈ (Arrow‘𝐶))
Theorem	arweuthinc 50606*	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 50607*	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 50608	Alternate definition of TermCat. See also df-termc 50550, dftermc2 50597. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat = {𝑐 ∣ (Arrow‘𝑐) ≈ 1o}
Theorem	termcfuncval 50609	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 50610	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 50611	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 50612	Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ TermCat)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑅 = (𝐴‘𝑋)    ⇒   ⊢ (𝜑 → 𝐴 = {⟨𝑋, 𝑅⟩})
Theorem	diag2f1olem 50613	Lemma for diag2f1o 50614. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝑀 ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌)))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑀‘𝑍)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝑀 = ((𝑋(2nd ‘𝐿)𝑌)‘𝐹)))
Theorem	diag2f1o 50614	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 50615	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 50616	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 50617	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 7770) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐶( ≃𝑐 ‘𝐸)𝑄)
Theorem	funcsn 50618	The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐶 Func 𝐷) = {𝐹})    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)
Theorem	fucterm 50619	The category of functors to a terminal category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)
Theorem	0fucterm 50620	The category of functors from an initial category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)
Theorem	termfucterm 50621	All functors between two terminal categories are isomorphisms. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ TermCat)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ TermCat)    ⇒   ⊢ (𝜑 → (𝑋 Func 𝑌) = (𝑋𝐼𝑌))
Theorem	cofuterm 50622	Post-compose with a functor to a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐾 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾)
Theorem	uobeqterm 50623	Universal objects and terminal categories. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐴 = (Base‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    ⇒   ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌))
Theorem	isinito4 50624	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 50625	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.51.16.4  Preordered sets as thin categories
Syntax	cprstc 50626	Class function defining preordered sets as categories.
class ProsetToCat
Definition	df-prstc 50627	Definition of the function converting a preordered set to a category. Justified by prsthinc 50541. 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 50530), by prstcnid 50630, prstchom 50639, and prstcthin 50638. Other important properties include prstcbas 50631, prstcleval 50632, prstcle 50633, prstcocval 50634, prstcoc 50635, prstchom2 50640, and prstcprs 50637. Use those instead. Note that the defining property prstchom 50639 is equivalent to prstchom2 50640 given prstcthin 50638. See thincn0eu 50508 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 50628	Lemma for prstcnidlem 50629 and prstcthin 50638. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Theorem	prstcnidlem 50629	Lemma for prstcnid 50630 and prstchomval 50636. (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 50630	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 50631	The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	prstcleval 50632	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 50633	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌))
Theorem	prstcocval 50634	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ⊥ = (oc‘𝐶))
Theorem	prstcoc 50635	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋))
Theorem	prstchomval 50636	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 50637	The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	prstcthin 50638	The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	prstchom 50639	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 50640*	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 50641). 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 50641*	Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 50627. See prstchom2 50640 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 50642	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 50643	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 50644	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 50645	Alternate proof of postcpos 50644. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset))
Theorem	postc 50646*	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 50647*	A singlegon is an element of the class of singlegons. The converse (basrestermcfolem 50648) also holds. This is trivial if 𝐵 is 𝑏 (abid 2743). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (∃𝑥 𝐵 = {𝑥} → 𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}})
Theorem	basrestermcfolem 50648*	An element of the class of singlegons is a singlegon. The converse (discsntermlem 50647) also holds. This is trivial if 𝐵 is 𝑏 (abid 2743). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} → ∃𝑥 𝐵 = {𝑥})
Theorem	discbas 50649	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 50650	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 50651*	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 50652*	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 50653	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 7770 is equivalent to sngl V ∉ V. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat ∉ V
21.51.16.5  Monoids as categories
Syntax	cmndtc 50654	Class function defining monoids as categories.
class MndToCat
Definition	df-mndtc 50655	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 50657), 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 mndtcbaseu 50658, mndtchom 50661, mndtcco 50662. 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 50656	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 50657	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	mndtcbaseu 50658*	The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵)
Theorem	mndtcob 50659	Lemma for mndtchom 50661 and mndtcco 50662. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑀)
Theorem	mndtcobeq 50660	Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	mndtchom 50661	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 50662	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 50663	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 50664*	Lemma for mndtccat 50665 and mndtcid 50666. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0g‘𝑀))))
Theorem	mndtccat 50665	The function value is a category. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	mndtcid 50666	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 50667	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 50668	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 50669	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 50670	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 50671	All morphisms in a category converted from a group are epimorphisms. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐸 = (Epi‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌))
21.51.16.6  Categories with at most one object and at most two morphisms
Theorem	2arwcatlem1 50672	Lemma for 2arwcat 50677. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝑋𝐻𝑋) = { 0 , 1 }    ⇒   ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
Theorem	2arwcatlem2 50673	Lemma for 2arwcat 50677. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) = 0 )    ⇒   ⊢ (𝜑 → ( 1 (⟨𝐴, 𝐵⟩ · 𝐶)𝐹) = 𝐹)
Theorem	2arwcatlem3 50674	Lemma for 2arwcat 50677. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 0 )    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐴, 𝐵⟩ · 𝐶) 1 ) = 𝐹)
Theorem	2arwcatlem4 50675	Lemma for 2arwcat 50677. (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 50676	Lemma for 2arwcat 50677. (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 50677*	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 17850, catrid 17851, and catcocl 17852. (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 50678*	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 50679*	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 50680*	Lemma for cnelsubc 50681. (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 50681*	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 17980 is necessary. A stronger statement than nelsubc3 50148. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat))
21.51.17  Kan extensions and related concepts
21.51.17.1  Kan extensions
Syntax	clan 50682	Class function defining the (local) left Kan extension.
class Lan
Syntax	cran 50683	Class function defining the (local) right Kan extension.
class Ran
Definition	df-lan 50684*	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 50704). 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 50704 (retrieved 3 Nov 2025). A left Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (lanrcl4 50711) and the second component is a natural transformation 𝐴:𝑋⟶𝐿𝐹 (lanrcl5 50712) 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 50685 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 50685*	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 50707). 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 50707 (retrieved 3 Nov 2025). A right Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (ranrcl4 50716) and the second component is a natural transformation 𝐴:𝐿𝐹⟶𝑋 (ranrcl5 50717) 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 50684 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 50686	Lan is a function on ((V × V) × V). (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Lan Fn ((V × V) × V)
Theorem	ranfn 50687	Ran is a function on ((V × V) × V). (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Ran Fn ((V × V) × V)
Theorem	reldmlan 50688	The domain of Lan is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom Lan
Theorem	reldmran 50689	The domain of Ran is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom Ran
Theorem	lanfval 50690*	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 50691*	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 50692	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 50693	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 50694	The domain of (𝑃 Lan 𝐸) is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom (𝑃 Lan 𝐸)
Theorem	reldmran2 50695	The domain of (𝑃 Ran 𝐸) is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom (𝑃 Ran 𝐸)
Theorem	lanval 50696	Value of the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = 𝐾)    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	ranval 50697	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 50698	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))
Theorem	ranrcl 50699	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))
Theorem	rellan 50700	The set of left Kan extensions is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel (𝐹(𝑃 Lan 𝐸)𝑋)