P. 500 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49901-50000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fucterm 49901	The category of functors to a terminal category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)
Theorem	0fucterm 49902	The category of functors from an initial category is terminal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    ⇒   ⊢ (𝜑 → 𝑄 ∈ TermCat)
Theorem	termfucterm 49903	All functors between two terminal categories are isomorphisms. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ TermCat)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ TermCat)    ⇒   ⊢ (𝜑 → (𝑋 Func 𝑌) = (𝑋𝐼𝑌))
Theorem	cofuterm 49904	Post-compose with a functor to a terminal category. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐾 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾)
Theorem	uobeqterm 49905	Universal objects and terminal categories. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐴 = (Base‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ TermCat)    &   ⊢ (𝜑 → 𝐸 ∈ TermCat)    ⇒   ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌))
Theorem	isinito4 49906	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 49907	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 49908	Class function defining preordered sets as categories.
class ProsetToCat
Definition	df-prstc 49909	Definition of the function converting a preordered set to a category. Justified by prsthinc 49823. 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 49812), by prstcnid 49912, prstchom 49921, and prstcthin 49920. Other important properties include prstcbas 49913, prstcleval 49914, prstcle 49915, prstcocval 49916, prstcoc 49917, prstchom2 49922, and prstcprs 49919. Use those instead. Note that the defining property prstchom 49921 is equivalent to prstchom2 49922 given prstcthin 49920. See thincn0eu 49790 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 49910	Lemma for prstcnidlem 49911 and prstcthin 49920. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Theorem	prstcnidlem 49911	Lemma for prstcnid 49912 and prstchomval 49918. (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 49912	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 49913	The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	prstcleval 49914	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 49915	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌))
Theorem	prstcocval 49916	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ⊥ = (oc‘𝐶))
Theorem	prstcoc 49917	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋))
Theorem	prstchomval 49918	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 49919	The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	prstcthin 49920	The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	prstchom 49921	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 49922*	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 49923). 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 49923*	Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 49909. See prstchom2 49922 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 49924	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 49925	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 49926	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 49927	Alternate proof of postcpos 49926. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset))
Theorem	postc 49928*	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 49929*	A singlegon is an element of the class of singlegons. The converse (basrestermcfolem 49930) also holds. This is trivial if 𝐵 is 𝑏 (abid 2719). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (∃𝑥 𝐵 = {𝑥} → 𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}})
Theorem	basrestermcfolem 49930*	An element of the class of singlegons is a singlegon. The converse (discsntermlem 49929) also holds. This is trivial if 𝐵 is 𝑏 (abid 2719). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} → ∃𝑥 𝐵 = {𝑥})
Theorem	discbas 49931	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 49932	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 49933*	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 49934*	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 49935	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 7713 is equivalent to sngl V ∉ V. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat ∉ V
21.49.16.5  Monoids as categories
Syntax	cmndtc 49936	Class function defining monoids as categories.
class MndToCat
Definition	df-mndtc 49937	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 49939), 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 49940, mndtchom 49943, mndtcco 49944. 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 49938	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 49939	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 49940*	The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵)
Theorem	mndtcob 49941	Lemma for mndtchom 49943 and mndtcco 49944. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑀)
Theorem	mndtcbas2 49942	Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	mndtchom 49943	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 49944	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 49945	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 49946*	Lemma for mndtccat 49947 and mndtcid 49948. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0g‘𝑀))))
Theorem	mndtccat 49947	The function value is a category. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	mndtcid 49948	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 49949	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 49950	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 49951	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 49952	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 49953	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 49954	Lemma for 2arwcat 49959. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝑋𝐻𝑋) = { 0 , 1 }    ⇒   ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
Theorem	2arwcatlem2 49955	Lemma for 2arwcat 49959. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) = 0 )    ⇒   ⊢ (𝜑 → ( 1 (⟨𝐴, 𝐵⟩ · 𝐶)𝐹) = 𝐹)
Theorem	2arwcatlem3 49956	Lemma for 2arwcat 49959. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 0 )    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐴, 𝐵⟩ · 𝐶) 1 ) = 𝐹)
Theorem	2arwcatlem4 49957	Lemma for 2arwcat 49959. (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 49958	Lemma for 2arwcat 49959. (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 49959*	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 17618, catrid 17619, and catcocl 17620. (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 49960*	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 49961*	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 49962*	Lemma for cnelsubc 49963. (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 49963*	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 17748 is necessary. A stronger statement than nelsubc3 49430. (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 49964	Class function defining the (local) left Kan extension.
class Lan
Syntax	cran 49965	Class function defining the (local) right Kan extension.
class Ran
Definition	df-lan 49966*	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 49986). 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 49986 (retrieved 3 Nov 2025). A left Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (lanrcl4 49993) and the second component is a natural transformation 𝐴:𝑋⟶𝐿𝐹 (lanrcl5 49994) 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 49967 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 49967*	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 49989). 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 49989 (retrieved 3 Nov 2025). A right Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (ranrcl4 49998) and the second component is a natural transformation 𝐴:𝐿𝐹⟶𝑋 (ranrcl5 49999) 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 49966 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 49968	Lan is a function on ((V × V) × V). (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Lan Fn ((V × V) × V)
Theorem	ranfn 49969	Ran is a function on ((V × V) × V). (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Ran Fn ((V × V) × V)
Theorem	reldmlan 49970	The domain of Lan is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom Lan
Theorem	reldmran 49971	The domain of Ran is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom Ran
Theorem	lanfval 49972*	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 49973*	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 49974	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 49975	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 49976	The domain of (𝑃 Lan 𝐸) is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom (𝑃 Lan 𝐸)
Theorem	reldmran2 49977	The domain of (𝑃 Ran 𝐸) is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom (𝑃 Ran 𝐸)
Theorem	lanval 49978	Value of the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = 𝐾)    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	ranval 49979	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 49980	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))
Theorem	ranrcl 49981	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))
Theorem	rellan 49982	The set of left Kan extensions is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel (𝐹(𝑃 Lan 𝐸)𝑋)
Theorem	relran 49983	The set of right Kan extensions is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel (𝐹(𝑃 Ran 𝐸)𝑋)
Theorem	islan 49984	A left Kan extension is a universal pair. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → 𝐿 ∈ (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	islan2 49985	A left Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴 → 𝐿(𝐾(𝑅 UP 𝑆)𝑋)𝐴)
Theorem	lanval2 49986	The set of left Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by isup2 49553 and upciclem1 49525. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	isran 49987	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 49988	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 49989	The set of right Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by oppcup2 49567 and oppcup3lem 49565. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) = (⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋))
Theorem	ranval3 49990	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 49991	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	lanrcl3 49992	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))
Theorem	lanrcl4 49993	The first component of a left Kan extension is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))
Theorem	lanrcl5 49994	The second component of a left Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝑁(𝐿 ∘func 𝐹)))
Theorem	ranrcl2 49995	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	ranrcl3 49996	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))
Theorem	ranrcl4lem 49997	Lemma for ranrcl4 49998 and ranrcl5 49999. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(1st ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)), (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹))⟩)
Theorem	ranrcl4 49998	The first component of a right Kan extension is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))
Theorem	ranrcl5 49999	The second component of a right Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ((𝐿 ∘func 𝐹)𝑁𝑋))
Theorem	lanup 50000*	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 𝐹))𝐴)))