P. 499 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49801-49900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prstcle 49801	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌))
Theorem	prstcocval 49802	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ⊥ = (oc‘𝐶))
Theorem	prstcoc 49803	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋))
Theorem	prstchomval 49804	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 49805	The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	prstcthin 49806	The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	prstchom 49807	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 49808*	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 49809). 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 49809*	Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 49795. See prstchom2 49808 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 49810	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 49811	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 49812	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 49813	Alternate proof of postcpos 49812. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset))
Theorem	postc 49814*	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 49815*	A singlegon is an element of the class of singlegons. The converse (basrestermcfolem 49816) also holds. This is trivial if 𝐵 is 𝑏 (abid 2718). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (∃𝑥 𝐵 = {𝑥} → 𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}})
Theorem	basrestermcfolem 49816*	An element of the class of singlegons is a singlegon. The converse (discsntermlem 49815) also holds. This is trivial if 𝐵 is 𝑏 (abid 2718). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} → ∃𝑥 𝐵 = {𝑥})
Theorem	discbas 49817	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 49818	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 49819*	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 49820*	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 49821	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 7703 is equivalent to sngl V ∉ V. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat ∉ V
21.49.16.5  Monoids as categories
Syntax	cmndtc 49822	Class function defining monoids as categories.
class MndToCat
Definition	df-mndtc 49823	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 49825), 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 49826, mndtchom 49829, mndtcco 49830. 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 49824	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 49825	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 49826*	The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵)
Theorem	mndtcob 49827	Lemma for mndtchom 49829 and mndtcco 49830. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑀)
Theorem	mndtcbas2 49828	Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	mndtchom 49829	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 49830	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 49831	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 49832*	Lemma for mndtccat 49833 and mndtcid 49834. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0g‘𝑀))))
Theorem	mndtccat 49833	The function value is a category. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	mndtcid 49834	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 49835	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 49836	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 49837	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 49838	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 49839	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 49840	Lemma for 2arwcat 49845. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝑋𝐻𝑋) = { 0 , 1 }    ⇒   ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
Theorem	2arwcatlem2 49841	Lemma for 2arwcat 49845. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) = 0 )    ⇒   ⊢ (𝜑 → ( 1 (⟨𝐴, 𝐵⟩ · 𝐶)𝐹) = 𝐹)
Theorem	2arwcatlem3 49842	Lemma for 2arwcat 49845. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 0 )    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐴, 𝐵⟩ · 𝐶) 1 ) = 𝐹)
Theorem	2arwcatlem4 49843	Lemma for 2arwcat 49845. (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 49844	Lemma for 2arwcat 49845. (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 49845*	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 17606, catrid 17607, and catcocl 17608. (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 49846*	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 49847*	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 49848*	Lemma for cnelsubc 49849. (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 49849*	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 17736 is necessary. A stronger statement than nelsubc3 49316. (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 49850	Class function defining the (local) left Kan extension.
class Lan
Syntax	cran 49851	Class function defining the (local) right Kan extension.
class Ran
Definition	df-lan 49852*	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 49872). 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 49872 (retrieved 3 Nov 2025). A left Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (lanrcl4 49879) and the second component is a natural transformation 𝐴:𝑋⟶𝐿𝐹 (lanrcl5 49880) 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 49853 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 49853*	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 49875). 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 49875 (retrieved 3 Nov 2025). A right Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (ranrcl4 49884) and the second component is a natural transformation 𝐴:𝐿𝐹⟶𝑋 (ranrcl5 49885) 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 49852 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 49854	Lan is a function on ((V × V) × V). (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Lan Fn ((V × V) × V)
Theorem	ranfn 49855	Ran is a function on ((V × V) × V). (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Ran Fn ((V × V) × V)
Theorem	reldmlan 49856	The domain of Lan is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom Lan
Theorem	reldmran 49857	The domain of Ran is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom Ran
Theorem	lanfval 49858*	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 49859*	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 49860	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 49861	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 49862	The domain of (𝑃 Lan 𝐸) is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom (𝑃 Lan 𝐸)
Theorem	reldmran2 49863	The domain of (𝑃 Ran 𝐸) is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom (𝑃 Ran 𝐸)
Theorem	lanval 49864	Value of the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = 𝐾)    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	ranval 49865	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 49866	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))
Theorem	ranrcl 49867	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))
Theorem	rellan 49868	The set of left Kan extensions is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel (𝐹(𝑃 Lan 𝐸)𝑋)
Theorem	relran 49869	The set of right Kan extensions is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel (𝐹(𝑃 Ran 𝐸)𝑋)
Theorem	islan 49870	A left Kan extension is a universal pair. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → 𝐿 ∈ (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	islan2 49871	A left Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴 → 𝐿(𝐾(𝑅 UP 𝑆)𝑋)𝐴)
Theorem	lanval2 49872	The set of left Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by isup2 49439 and upciclem1 49411. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	isran 49873	A right Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋))    ⇒   ⊢ (𝜑 → 𝐿 ∈ (⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋))
Theorem	isran2 49874	A right Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿(⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋)𝐴)
Theorem	ranval2 49875	The set of right Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by oppcup2 49453 and oppcup3lem 49451. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) = (⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋))
Theorem	ranval3 49876	The set of right Kan extensions is the set of universal pairs. (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) = (( oppFunc ‘𝐾)(𝑂 UP 𝑃)𝑋))
Theorem	lanrcl2 49877	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	lanrcl3 49878	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))
Theorem	lanrcl4 49879	The first component of a left Kan extension is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))
Theorem	lanrcl5 49880	The second component of a left Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝑁(𝐿 ∘func 𝐹)))
Theorem	ranrcl2 49881	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	ranrcl3 49882	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))
Theorem	ranrcl4lem 49883	Lemma for ranrcl4 49884 and ranrcl5 49885. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(1st ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)), (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹))⟩)
Theorem	ranrcl4 49884	The first component of a right Kan extension is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))
Theorem	ranrcl5 49885	The second component of a right Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ((𝐿 ∘func 𝐹)𝑁𝑋))
Theorem	lanup 49886*	The universal property of the left Kan extension; expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝑀 = (𝐷 Nat 𝐸)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    &   ⊢ ∙ = (comp‘𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝑁(𝐿 ∘func 𝐹)))    ⇒   ⊢ (𝜑 → (𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴 ↔ ∀𝑙 ∈ (𝐷 Func 𝐸)∀𝑎 ∈ (𝑋𝑁(𝑙 ∘func 𝐹))∃!𝑏 ∈ (𝐿𝑀𝑙)𝑎 = ((𝑏 ∘ (1st ‘𝐹))(⟨𝑋, (𝐿 ∘func 𝐹)⟩ ∙ (𝑙 ∘func 𝐹))𝐴)))
Theorem	ranup 49887*	The universal property of the right Kan extension; expressed explicitly. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝑀 = (𝐷 Nat 𝐸)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    &   ⊢ ∙ = (comp‘𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ ((𝐿 ∘func 𝐹)𝑁𝑋))    ⇒   ⊢ (𝜑 → (𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴 ↔ ∀𝑙 ∈ (𝐷 Func 𝐸)∀𝑎 ∈ ((𝑙 ∘func 𝐹)𝑁𝑋)∃!𝑏 ∈ (𝑙𝑀𝐿)𝑎 = (𝐴(⟨(𝑙 ∘func 𝐹), (𝐿 ∘func 𝐹)⟩ ∙ 𝑋)(𝑏 ∘ (1st ‘𝐹)))))
21.49.17.2  Limits and colimits
Syntax	clmd 49888	Class function defining the limit of a diagram.
class Limit
Syntax	ccmd 49889	Class function defining the colimit of a diagram.
class Colimit
Definition	df-lmd 49890*	A diagram of type 𝐷 or a 𝐷-shaped diagram in a category 𝐶, is a functor 𝐹:𝐷⟶𝐶 where the source category 𝐷, usually small or even finite, is called the index category or the scheme of the diagram. The actual objects and morphisms in 𝐷 are largely irrelevant; only the way in which they are interrelated matters. The diagram is thought of as indexing a collection of objects and morphisms in 𝐶 patterned on 𝐷. Definition 11.1(1) of [Adamek] p. 193. A cone to a diagram, or a natural source for a diagram in a category 𝐶 is a pair of an object 𝑋 in 𝐶 and a natural transformation from the constant functor (or constant diagram) of the object 𝑋 to the diagram. The second component associates each object in the index category with a morphism in 𝐶 whose domain is 𝑋 (concl 49906). The naturality guarantees that the combination of the diagram with the cone must commute (concom 49908). Definition 11.3(1) of [Adamek] p. 193. A limit of a diagram 𝐹:𝐷⟶𝐶 of type 𝐷 in category 𝐶 is a universal pair from the diagonal functor (𝐶Δfunc𝐷) to the diagram. The universal pair is a cone to the diagram satisfying the universal property, that each cone to the diagram uniquely factors through the limit (islmd 49910). Definition 11.3(2) of [Adamek] p. 194. Terminal objects (termolmd 49915), products, equalizers, pullbacks, and inverse limits can be considered as limits of some diagram; limits can be further generalized as right Kan extensions (lmdran 49916). "lmd" is short for "limit of a diagram". See df-cmd 49891 for the dual concept (lmddu 49912, cmddu 49913). (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Limit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ (( oppFunc ‘(𝑐Δfunc𝑑))((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))𝑓)))
Definition	df-cmd 49891*	A co-cone (or cocone) to a diagram (see df-lmd 49890 for definition), or a natural sink for a diagram in a category 𝐶 is a pair of an object 𝑋 in 𝐶 and a natural transformation from the diagram to the constant functor (or constant diagram) of the object 𝑋. The second component associates each object in the index category with a morphism in 𝐶 whose codomain is 𝑋 (coccl 49907). The naturality guarantees that the combination of the diagram with the co-cone must commute (coccom 49909). Definition 11.27(1) of [Adamek] p. 202. A colimit of a diagram 𝐹:𝐷⟶𝐶 of type 𝐷 in category 𝐶 is a universal pair from the diagram to the diagonal functor (𝐶Δfunc𝐷). The universal pair is a co-cone to the diagram satisfying the universal property, that each co-cone to the diagram uniquely factors through the colimit. (iscmd 49911). Definition 11.27(2) of [Adamek] p. 202. Initial objects (initocmd 49914), coproducts, coequalizers, pushouts, and direct limits can be considered as colimits of some diagram; colimits can be further generalized as left Kan extensions (cmdlan 49917). "cmd" is short for "colimit of a diagram". See df-lmd 49890 for the dual concept (lmddu 49912, cmddu 49913). (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Colimit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓)))
Theorem	reldmlmd 49892	The domain of Limit is a relation. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Rel dom Limit
Theorem	reldmcmd 49893	The domain of Colimit is a relation. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Rel dom Colimit
Theorem	lmdfval 49894*	Function value of Limit. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝐶 Limit 𝐷) = (𝑓 ∈ (𝐷 Func 𝐶) ↦ (( oppFunc ‘(𝐶Δfunc𝐷))((oppCat‘𝐶) UP (oppCat‘(𝐷 FuncCat 𝐶)))𝑓))
Theorem	cmdfval 49895*	Function value of Colimit. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ (𝐶 Colimit 𝐷) = (𝑓 ∈ (𝐷 Func 𝐶) ↦ ((𝐶Δfunc𝐷)(𝐶 UP (𝐷 FuncCat 𝐶))𝑓))
Theorem	lmdrcl 49896	Reverse closure for a limit of a diagram. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝑋 ∈ ((𝐶 Limit 𝐷)‘𝐹) → 𝐹 ∈ (𝐷 Func 𝐶))
Theorem	cmdrcl 49897	Reverse closure for a colimit of a diagram. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝑋 ∈ ((𝐶 Colimit 𝐷)‘𝐹) → 𝐹 ∈ (𝐷 Func 𝐶))
Theorem	reldmlmd2 49898	The domain of (𝐶 Limit 𝐷) is a relation. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ Rel dom (𝐶 Limit 𝐷)
Theorem	reldmcmd2 49899	The domain of (𝐶 Colimit 𝐷) is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel dom (𝐶 Colimit 𝐷)
Theorem	lmdfval2 49900	The set of limits of a diagram. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ ((𝐶 Limit 𝐷)‘𝐹) = (( oppFunc ‘(𝐶Δfunc𝐷))((oppCat‘𝐶) UP (oppCat‘(𝐷 FuncCat 𝐶)))𝐹)