P. 510 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50901-51000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prstcprs 50901	The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	prstcthin 50902	The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	prstchom 50903	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 50904*	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 50905). 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 50905*	Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 50891. See prstchom2 50904 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 50906	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 50907	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 50908	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 50909	Alternate proof of postcpos 50908. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset))
Theorem	postc 50910*	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 50911*	A singlegon is an element of the class of singlegons. The converse (basrestermcfolem 50912) also holds. This is trivial if 𝐵 is 𝑏 (abid 2745). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (∃𝑥 𝐵 = {𝑥} → 𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}})
Theorem	basrestermcfolem 50912*	An element of the class of singlegons is a singlegon. The converse (discsntermlem 50911) also holds. This is trivial if 𝐵 is 𝑏 (abid 2745). (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ {𝑏 ∣ ∃𝑥 𝑏 = {𝑥}} → ∃𝑥 𝐵 = {𝑥})
Theorem	discbas 50913	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 50914	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 50915*	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 50916*	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 50917	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 7793 is equivalent to sngl V ∉ V. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ TermCat ∉ V
21.53.16.5  Monoids as categories
Syntax	cmndtc 50918	Class function defining monoids as categories.
class MndToCat
Definition	df-mndtc 50919	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 50921), 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 50922, mndtchom 50925, mndtcco 50926. 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 50920	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 50921	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 50922*	The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵)
Theorem	mndtcob 50923	Lemma for mndtchom 50925 and mndtcco 50926. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑀)
Theorem	mndtcobeq 50924	Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	mndtchom 50925	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 50926	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 50927	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 50928*	Lemma for mndtccat 50929 and mndtcid 50930. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ (0g‘𝑀))))
Theorem	mndtccat 50929	The function value is a category. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	mndtcid 50930	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 50931	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 50932	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 50933	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 50934	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 50935	All morphisms in a category converted from a group are epimorphisms. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐸 = (Epi‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌))
21.53.16.6  Categories with at most one object and at most two morphisms
Theorem	2arwcatlem1 50936	Lemma for 2arwcat 50941. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝑋𝐻𝑋) = { 0 , 1 }    ⇒   ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
Theorem	2arwcatlem2 50937	Lemma for 2arwcat 50941. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 0 ) = 0 )    ⇒   ⊢ (𝜑 → ( 1 (⟨𝐴, 𝐵⟩ · 𝐶)𝐹) = 𝐹)
Theorem	2arwcatlem3 50938	Lemma for 2arwcat 50941. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝑋)    &   ⊢ (𝜑 → 𝐵 = 𝑌)    &   ⊢ (𝜑 → 𝐶 = 𝑍)    &   ⊢ (𝜑 → (𝐹 = 0 ∨ 𝐹 = 1 ))    &   ⊢ (𝜑 → ( 1 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 1 )    &   ⊢ (𝜑 → ( 0 (⟨𝑋, 𝑌⟩ · 𝑍) 1 ) = 0 )    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐴, 𝐵⟩ · 𝐶) 1 ) = 𝐹)
Theorem	2arwcatlem4 50939	Lemma for 2arwcat 50941. (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 50940	Lemma for 2arwcat 50941. (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 50941*	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 17883, catrid 17884, and catcocl 17885. (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 50942*	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 50943*	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	cnelsubcw 50944*	A weaker version of cnelsubc 50945, which requires fewer axioms. (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 50945*	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 18013 is necessary. A stronger statement than nelsubc3 50388. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ ¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ (𝑐 ↾cat 𝑗) ∈ Cat))
21.53.16.7  Parallel-arrow categories
Theorem	parhomval 50946*	At objects in the base, the hom operation has value {𝐽} on the diagonal, 𝑆 from the distinguished source to target, and the empty set otherwise. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ ((𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝑈𝐻𝑉) = if(𝑈 = 𝑉, {𝐽}, if((𝑈 = 𝑋 ∧ 𝑉 = 𝑌), 𝑆, ∅)))
Theorem	parhomel 50947*	Membership in a hom-set of a parallel-arrow category is equivalent to being its identity value on the diagonal, or a member of 𝑆 at the distinguished source and target. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    ⇒   ⊢ ((𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹 ∈ (𝑈𝐻𝑉) ↔ ((𝑈 = 𝑉 ∧ 𝐹 = 𝐽) ∨ (¬ 𝑈 = 𝑉 ∧ ((𝑈 = 𝑋 ∧ 𝑉 = 𝑌) ∧ 𝐹 ∈ 𝑆)))))
Theorem	parhomcl2 50948*	Variant of parhomcl 50951. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ 𝐾 = (𝑆 ∪ {𝐽})    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐾)
Theorem	parhomidval 50949*	On the diagonal, the parallel-arrow hom operation has value {𝐽}. (Contributed by Zhi Wang, 16-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    ⇒   ⊢ (𝑈 ∈ 𝐵 → (𝑈𝐻𝑈) = {𝐽})
Theorem	parhomssun 50950*	Every value of the parallel-arrow hom operation is a subclass of the arrow carrier. (Contributed by Zhi Wang, 16-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝐾 = (𝑆 ∪ {𝐽})    ⇒   ⊢ (𝑈𝐻𝑉) ⊆ 𝐾
Theorem	parhomcl 50951*	All hom-sets of the parallel-arrow construction lie in its arrow carrier. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 16-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝐾 = (𝑆 ∪ {𝐽})    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐾)
Theorem	parhomideq2 50952*	Variant of parhomideq 50953. (Contributed by Zhi Wang, 14-Sep-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → 𝑈 = 𝑉)    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐽)
Theorem	parhomideq 50953*	An endomorphism in the parallel-arrow construction has the identity value. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 16-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → 𝑈 = 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐽)
Theorem	parhomid2 50954*	Variant of parhomid 50955. (Contributed by Zhi Wang, 14-Sep-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝐽 ∈ V    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ (𝜑 → 𝐽 ∈ (𝑈𝐻𝑈))
Theorem	parhomid 50955*	The identity value belongs to each endomorphism hom-set. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 16-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝐽 ∈ V    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐽 ∈ (𝑈𝐻𝑈))
Theorem	parhomvaln0 50956*	Evaluate an inhabited parallel-arrow hom-set. Membership certifies the selected branch even when sethood hypotheses are unavailable. Compare parhomval 50946 for evaluation throughout the object domain. (Contributed by Zhi Wang, 17-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    ⇒   ⊢ (𝐹 ∈ (𝑈𝐻𝑉) → (𝑈𝐻𝑉) = if(𝑈 = 𝑉, {𝐽}, if((𝑈 = 𝑋 ∧ 𝑉 = 𝑌), 𝑆, ∅)))
Theorem	parhomne2 50957*	Variant of parhomne 50958. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → ¬ 𝑈 = 𝑉)    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑈 = 𝑋 ∧ 𝑉 = 𝑌))
Theorem	parhomne 50958*	A morphism between different objects has the distinguished source and target. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → ¬ 𝑈 = 𝑉)    ⇒   ⊢ (𝜑 → (𝑈 = 𝑋 ∧ 𝑉 = 𝑌))
Theorem	parhomss2 50959*	Variant of parhomss 50960. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ⊆ 𝐽)
Theorem	parhomss 50960*	When every member of the parallel-arrow class 𝑆 is a subset of 𝐽, every arrow in a hom-set is a subset of its identity value 𝐽. The subset hypothesis is essential; it does not follow from the hom-set definition alone. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    ⇒   ⊢ (𝜑 → 𝐹 ⊆ 𝐽)
Theorem	parhomeqor2 50961*	Variant of parhomeqor 50962. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑉𝐻𝑊))    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ 𝑋 ≠ 𝑌    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑈 = 𝑉 ∨ 𝑉 = 𝑊))
Theorem	parhomeqor 50962*	In a composable pair, at least one arrow is an endomorphism. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑉𝐻𝑊))    ⇒   ⊢ (𝜑 → (𝑈 = 𝑉 ∨ 𝑉 = 𝑊))
Theorem	parhomco2 50963*	Variant of parhomco 50964. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑉𝐻𝑊))    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ 𝑋 ≠ 𝑌    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 ∩ 𝐹) ∈ (𝑈𝐻𝑊))
Theorem	parhomco 50964*	When every member of the parallel-arrow class 𝑆 is a subset of 𝐽, intersection of composable arrows belongs to the hom-set from the first object to the last. The subset hypothesis supplies the required intersection identity laws; it does not follow from the hom construction alone. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑉𝐻𝑊))    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    ⇒   ⊢ (𝜑 → (𝐺 ∩ 𝐹) ∈ (𝑈𝐻𝑊))
Theorem	parcoval 50965*	The composition in the specified parallel-arrow categories is intersection. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝑀 = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐾 ↦ (𝑓 ∩ 𝑔))    &   ⊢ · = (𝑝 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ 𝑀)    &   ⊢ 𝑀 ∈ V    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑈, 𝑉⟩ · 𝑊)𝐹) = (𝐺 ∩ 𝐹))
Theorem	parcatid2 50966*	Variant of parcatid 50967. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    &   ⊢ 𝐾 = (𝑆 ∪ {𝐽})    &   ⊢ 𝐻 = (𝑚 ∈ 𝐵, 𝑛 ∈ 𝐵 ↦ if(𝑚 = 𝑛, {𝐽}, if((𝑚 = 𝑋 ∧ 𝑛 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝑀 = (𝑟 ∈ 𝐾, 𝑠 ∈ 𝐾 ↦ (𝑟 ∩ 𝑠))    &   ⊢ · = (𝑝 ∈ (𝐵 × 𝐵), 𝑞 ∈ 𝐵 ↦ 𝑀)    &   ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩}    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝑋 ≠ 𝑌    ⇒   ⊢ (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐽))
Theorem	parcatid 50967*	Construct a category with a family of parallel arrows from 𝑋 to 𝑌 and only identity endomorphisms. All arrow values are subsets of 𝐽; composition is intersection. Nonidentity arrows can occur only when 𝑋 and 𝑌 are distinct members of 𝐵. If 𝑋 = 𝑌, or either distinguished endpoint is outside 𝐵, the category is discrete. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    &   ⊢ 𝐾 = (𝑆 ∪ {𝐽})    &   ⊢ 𝐻 = (𝑚 ∈ 𝐵, 𝑛 ∈ 𝐵 ↦ if(𝑚 = 𝑛, {𝐽}, if((𝑚 = 𝑋 ∧ 𝑛 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝑀 = (𝑟 ∈ 𝐾, 𝑠 ∈ 𝐾 ↦ (𝑟 ∩ 𝑠))    &   ⊢ · = (𝑝 ∈ (𝐵 × 𝐵), 𝑞 ∈ 𝐵 ↦ 𝑀)    &   ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩}    ⇒   ⊢ (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐽))
Theorem	paridval 50968*	The identity at any object of a category with the parallel-arrow hom construction is 𝐽. (Contributed by Zhi Wang, 17-Sep-2026.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((Id‘𝐶)‘𝑈) = 𝐽)
Theorem	parcoval2 50969*	Composition in a category with the parallel-arrow hom construction. Every composable pair contains an identity, so the category identity laws determine the value. (Contributed by Zhi Wang, 17-Sep-2026.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑉𝐻𝑊))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑈, 𝑉⟩ · 𝑊)𝐹) = if(𝑈 = 𝑉, 𝐺, 𝐹))
Theorem	par2catid 50970*	A concrete category with two objects and two parallel nonidentity arrows. The two identity arrows both have raw value 2o; their sources and targets distinguish them. The parallel arrows have raw values the empty set and 1o. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐶 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    ⇒   ⊢ (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 2o ↦ 2o))
Theorem	par2cat 50971*	The explicitly given two-object, two-parallel-arrow category exists. This closed theorem discharges the constructor premises in par2catid 50970. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩} ∈ Cat
Theorem	par2str 50972*	The object set, hom operation, and composition of the concrete two-object parallel-arrow category. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐶 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    ⇒   ⊢ (2o = (Base‘𝐶) ∧ (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅))) = (Hom ‘𝐶) ∧ (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠))) = (comp‘𝐶))
Theorem	parmapcl2 50973*	Variant of parmapcl 50974. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → (𝐴‘𝐽) = 𝐽)    &   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑆) → (𝐴‘𝐹) ∈ 𝑆)    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴‘𝐹) ∈ (𝑈𝐻𝑉))
Theorem	parmapcl 50974*	A map fixing the identity value and preserving the parallel-arrow class preserves each hom-set. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → (𝐴‘𝐽) = 𝐽)    &   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑆) → (𝐴‘𝐹) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴‘𝐹) ∈ (𝑈𝐻𝑉))
Theorem	parmapco2 50975*	Variant of parmapco 50976. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → (𝐴‘𝐽) = 𝐽)    &   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑆) → (𝐴‘𝐹) ∈ 𝑆)    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    &   ⊢ 𝑋 ≠ 𝑌    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑉𝐻𝑊))    &   ⊢ ((𝜑 ∧ 𝐺 ∈ 𝑆) → (𝐴‘𝐺) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴‘(𝐺 ∩ 𝐹)) = ((𝐴‘𝐺) ∩ (𝐴‘𝐹)))
Theorem	parmapco 50976*	An identity-fixing map preserving parallel arrows preserves every typed composition. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝑥 = 𝑦, {𝐽}, if((𝑥 = 𝑋 ∧ 𝑦 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈𝐻𝑉))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑉𝐻𝑊))    &   ⊢ (𝜑 → (𝐴‘𝐽) = 𝐽)    &   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑆) → (𝐴‘𝐹) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝐺 ∈ 𝑆) → (𝐴‘𝐺) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴‘(𝐺 ∩ 𝐹)) = ((𝐴‘𝐺) ∩ (𝐴‘𝐹)))
Theorem	parmapfunc2 50977*	Variant of parmapfunc 50978. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐶 ∈ Cat    &   ⊢ 𝐻 = (𝑟 ∈ 𝐵, 𝑠 ∈ 𝐵 ↦ if(𝑟 = 𝑠, {𝐽}, if((𝑟 = 𝑋 ∧ 𝑠 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝐿 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑎 ∈ (𝑢𝐻𝑣) ↦ (𝐴‘𝑎)))    &   ⊢ (𝐴‘𝐽) = 𝐽    &   ⊢ ∀𝑡 ∈ 𝑆 (𝐴‘𝑡) ∈ 𝑆    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐽 ∈ V    &   ⊢ 𝑆 ⊆ 𝒫 𝐽    &   ⊢ 𝑋 ≠ 𝑌    &   ⊢ 𝐾 = (𝑆 ∪ {𝐽})    &   ⊢ 𝑀 = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐾 ↦ (𝑓 ∩ 𝑔))    &   ⊢ · = (𝑝 ∈ (𝐵 × 𝐵), 𝑞 ∈ 𝐵 ↦ 𝑀)    &   ⊢ 𝐼 = (𝑡 ∈ 𝐵 ↦ 𝐽)    ⇒   ⊢ ( I ↾ 𝐵)(𝐶 Func 𝐶)𝐿
Theorem	parmapfunc 50978*	A map fixing the identity value and preserving the parallel-arrow class induces an endofunctor fixing every object. Category membership and the hom construction suffice: every composable pair contains an identity. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐶 ∈ Cat    &   ⊢ 𝐻 = (𝑟 ∈ 𝐵, 𝑠 ∈ 𝐵 ↦ if(𝑟 = 𝑠, {𝐽}, if((𝑟 = 𝑋 ∧ 𝑠 = 𝑌), 𝑆, ∅)))    &   ⊢ 𝐿 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑎 ∈ (𝑢𝐻𝑣) ↦ (𝐴‘𝑎)))    &   ⊢ (𝐴‘𝐽) = 𝐽    &   ⊢ ∀𝑡 ∈ 𝑆 (𝐴‘𝑡) ∈ 𝑆    ⇒   ⊢ ( I ↾ 𝐵)(𝐶 Func 𝐶)𝐿
Theorem	parswapval 50979*	Evaluate the transposition of the two parallel-arrow values. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐴 = (𝑏 ∈ 3o ↦ if(𝑏 = 2o, 2o, if(𝑏 = ∅, 1o, ∅)))    ⇒   ⊢ (𝑈 ∈ 3o → (𝐴‘𝑈) = if(𝑈 = 2o, 2o, if(𝑈 = ∅, 1o, ∅)))
Theorem	parswapprop 50980*	The concrete transposition fixes the identity, preserves the parallel arrows, and sends the empty-set arrow to the ordinal-one arrow. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐴 = (𝑏 ∈ 3o ↦ if(𝑏 = 2o, 2o, if(𝑏 = ∅, 1o, ∅)))    ⇒   ⊢ ((𝐴‘2o) = 2o ∧ ∀𝑡 ∈ 2o (𝐴‘𝑡) ∈ 2o ∧ (𝐴‘∅) = 1o)
Theorem	parswapfunc 50981*	The explicit exchange of the two parallel nonidentity arrows is an endofunctor with identity object function. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐶 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    &   ⊢ 𝐴 = (𝑏 ∈ 3o ↦ if(𝑏 = 2o, 2o, if(𝑏 = ∅, 1o, ∅)))    &   ⊢ 𝐿 = (𝑢 ∈ 2o, 𝑣 ∈ 2o ↦ (𝑎 ∈ (𝑢(𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))𝑣) ↦ (𝐴‘𝑎)))    ⇒   ⊢ ⟨( I ↾ 2o), 𝐿⟩ ∈ (𝐶 Func 𝐶)
Theorem	par2hom 50982*	The four hom-sets of the explicit two-object parallel-arrow category. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐻 = (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))    ⇒   ⊢ ((∅𝐻∅) = {2o} ∧ (1o𝐻1o) = {2o} ∧ ((∅𝐻1o) = 2o ∧ (1o𝐻∅) = ∅))
Theorem	par2diag 50983*	Two constant functors into the concrete parallel-arrow category and a natural transformation whose component is the empty-set arrow. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐶 = (SetCat‘1o)    &   ⊢ 𝐸 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    &   ⊢ 𝐿 = (𝐸Δfunc𝐶)    &   ⊢ 𝐹 = ((1st ‘𝐿)‘∅)    &   ⊢ 𝐺 = ((1st ‘𝐿)‘1o)    &   ⊢ 𝐴 = (1o × {∅})    ⇒   ⊢ ((𝐹 ∈ (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) ∧ (𝐴 ∈ (𝐹(𝐶 Nat 𝐸)𝐺) ∧ (𝐴‘∅) = ∅) ∧ (((1st ‘𝐹)‘∅) = ∅ ∧ ((1st ‘𝐺)‘∅) = 1o))
21.53.16.8  Nonuniqueness of the morphism part of functor composition
Theorem	fuconuniqlem 50984*	Lemma for fuconuniq 50985. (Contributed by Zhi Wang, 14-Sep-2026.) (New usage is discouraged.)
⊢ 𝐶 = (SetCat‘1o)    &   ⊢ 𝐸 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐿 = (⟨𝐶, 𝐶⟩ ∘F 𝐸)    &   ⊢ 𝐴 = (𝑏 ∈ 3o ↦ if(𝑏 = 2o, 2o, if(𝑏 = ∅, 1o, ∅)))    &   ⊢ 𝑀 = (𝑢 ∈ 2o, 𝑣 ∈ 2o ↦ (𝑎 ∈ (𝑢(𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))𝑣) ↦ (𝐴‘𝑎)))    &   ⊢ 𝑆 = ⟨( I ↾ 2o), 𝑀⟩    &   ⊢ 𝑅 = (𝐸 FuncCat 𝐸)    &   ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐸⟩ ∘F 𝐸))    &   ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝑆)    &   ⊢ 𝑇 = ((𝐶 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐶))    &   ⊢ 𝐷 = (𝐸Δfunc𝐶)    &   ⊢ 𝐹 = ((1st ‘𝐷)‘∅)    &   ⊢ 𝐺 = ((1st ‘𝐷)‘1o)    &   ⊢ 𝑁 = (1o × {∅})    ⇒   ⊢ ((1st ‘𝐿)(𝑇 Func 𝑄)(2nd ‘(𝐾 ∘func 𝐿)) ∧ (2nd ‘(𝐾 ∘func 𝐿)) ≠ (2nd ‘𝐿))
Theorem	fuconuniq 50985*	The arrow map 𝐴 fixes the identity arrow 2o and exchanges the two nonidentity parallel arrows ∅ and 1o. It gives a concrete alternative to functor composition with the same object function and a different morphism function. All hypotheses name explicit constructed sets; no category or functor existence is assumed. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐶 = (SetCat‘1o)    &   ⊢ 𝐸 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐿 = (⟨𝐶, 𝐶⟩ ∘F 𝐸)    &   ⊢ 𝐴 = (𝑏 ∈ 3o ↦ if(𝑏 = 2o, 2o, if(𝑏 = ∅, 1o, ∅)))    &   ⊢ 𝑀 = (𝑢 ∈ 2o, 𝑣 ∈ 2o ↦ (𝑎 ∈ (𝑢(𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))𝑣) ↦ (𝐴‘𝑎)))    &   ⊢ 𝑆 = ⟨( I ↾ 2o), 𝑀⟩    &   ⊢ 𝑅 = (𝐸 FuncCat 𝐸)    &   ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐸⟩ ∘F 𝐸))    &   ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝑆)    &   ⊢ 𝑇 = ((𝐶 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐶))    ⇒   ⊢ ((1st ‘𝐿)(𝑇 Func 𝑄)(2nd ‘(𝐾 ∘func 𝐿)) ∧ (2nd ‘(𝐾 ∘func 𝐿)) ≠ (2nd ‘𝐿))
Theorem	fuconuniqvalslem 50986*	Lemma for fuconuniqvals 50987. (Contributed by Zhi Wang, 14-Sep-2026.) (New usage is discouraged.)
⊢ 𝐶 = (SetCat‘1o)    &   ⊢ 𝐸 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐿 = (⟨𝐶, 𝐶⟩ ∘F 𝐸)    &   ⊢ 𝐴 = (𝑏 ∈ 3o ↦ if(𝑏 = 2o, 2o, if(𝑏 = ∅, 1o, ∅)))    &   ⊢ 𝑀 = (𝑢 ∈ 2o, 𝑣 ∈ 2o ↦ (𝑎 ∈ (𝑢(𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))𝑣) ↦ (𝐴‘𝑎)))    &   ⊢ 𝑆 = ⟨( I ↾ 2o), 𝑀⟩    &   ⊢ 𝑅 = (𝐸 FuncCat 𝐸)    &   ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐸⟩ ∘F 𝐸))    &   ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝑆)    &   ⊢ 𝐷 = (𝐸Δfunc𝐶)    &   ⊢ 𝐹 = ((1st ‘𝐷)‘∅)    &   ⊢ 𝐺 = ((1st ‘𝐷)‘1o)    &   ⊢ 𝑁 = (1o × {∅})    &   ⊢ 𝑇 = ((𝐶 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐶))    ⇒   ⊢ (((𝑁(⟨𝐹, (idfunc‘𝐶)⟩(2nd ‘𝐿)⟨𝐺, (idfunc‘𝐶)⟩)((Id‘(𝐶 FuncCat 𝐶))‘(idfunc‘𝐶)))‘∅) = ∅ ∧ ((𝑁(⟨𝐹, (idfunc‘𝐶)⟩(2nd ‘(𝐾 ∘func 𝐿))⟨𝐺, (idfunc‘𝐶)⟩)((Id‘(𝐶 FuncCat 𝐶))‘(idfunc‘𝐶)))‘∅) = 1o)
Theorem	fuconuniqvals 50987*	At the same natural-transformation/identity input, the canonical and alternative morphism maps give respectively ∅ and 1o at the unique source object ∅. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)
⊢ 𝐶 = (SetCat‘1o)    &   ⊢ 𝐸 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐿 = (⟨𝐶, 𝐶⟩ ∘F 𝐸)    &   ⊢ 𝐴 = (𝑏 ∈ 3o ↦ if(𝑏 = 2o, 2o, if(𝑏 = ∅, 1o, ∅)))    &   ⊢ 𝑀 = (𝑢 ∈ 2o, 𝑣 ∈ 2o ↦ (𝑎 ∈ (𝑢(𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))𝑣) ↦ (𝐴‘𝑎)))    &   ⊢ 𝑆 = ⟨( I ↾ 2o), 𝑀⟩    &   ⊢ 𝑅 = (𝐸 FuncCat 𝐸)    &   ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐸⟩ ∘F 𝐸))    &   ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝑆)    &   ⊢ 𝐷 = (𝐸Δfunc𝐶)    &   ⊢ 𝐹 = ((1st ‘𝐷)‘∅)    &   ⊢ 𝐺 = ((1st ‘𝐷)‘1o)    &   ⊢ 𝑁 = (1o × {∅})    ⇒   ⊢ (((𝑁(⟨𝐹, (idfunc‘𝐶)⟩(2nd ‘𝐿)⟨𝐺, (idfunc‘𝐶)⟩)((Id‘(𝐶 FuncCat 𝐶))‘(idfunc‘𝐶)))‘∅) = ∅ ∧ ((𝑁(⟨𝐹, (idfunc‘𝐶)⟩(2nd ‘(𝐾 ∘func 𝐿))⟨𝐺, (idfunc‘𝐶)⟩)((Id‘(𝐶 FuncCat 𝐶))‘(idfunc‘𝐶)))‘∅) = 1o)
Theorem	fuconuniq2 50988*	The concrete parallel-arrow category supplies a morphism function different from canonical functor composition, with its object function fixed exactly. See par2cat 50971 and par2hom 50982 for the category and its four hom-sets. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ 𝐶 = (SetCat‘1o)    &   ⊢ 𝐸 = {⟨(Base‘ndx), 2o⟩, ⟨(Hom ‘ndx), (𝑚 ∈ 2o, 𝑛 ∈ 2o ↦ if(𝑚 = 𝑛, {2o}, if((𝑚 = ∅ ∧ 𝑛 = 1o), 2o, ∅)))⟩, ⟨(comp‘ndx), (𝑝 ∈ (2o × 2o), 𝑞 ∈ 2o ↦ (𝑟 ∈ 3o, 𝑠 ∈ 3o ↦ (𝑟 ∩ 𝑠)))⟩}    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐿 = (⟨𝐶, 𝐶⟩ ∘F 𝐸)    &   ⊢ 𝑇 = ((𝐶 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐶))    ⇒   ⊢ ∃𝑧((1st ‘𝐿)(𝑇 Func 𝑄)𝑧 ∧ 𝑧 ≠ (2nd ‘𝐿))
Theorem	fuconuniqex 50989*	The object function of functor composition does not in general determine its morphism function, even when both source categories are the trivial category. The witness category is the explicit two-object, two-parallel-arrow category of par2cat 50971. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ ∃𝑒 ∈ Cat ∃𝑧((1st ‘(⟨(SetCat‘1o), (SetCat‘1o)⟩ ∘F 𝑒))((((SetCat‘1o) FuncCat 𝑒) ×c ((SetCat‘1o) FuncCat (SetCat‘1o))) Func ((SetCat‘1o) FuncCat 𝑒))𝑧 ∧ 𝑧 ≠ (2nd ‘(⟨(SetCat‘1o), (SetCat‘1o)⟩ ∘F 𝑒)))
Theorem	fuconuniqex2 50990*	There are categories for which the object function of functor composition does not determine its morphism function. Choose both source categories to be the trivial category and apply fuconuniqex 50989. The full compatibility conditions are given in fucoisfunc 50690; fucoisfunc2 50693 expands the natural-transformation component conditions. (Contributed by Zhi Wang, 14-Sep-2026.)
⊢ ∃𝑐 ∈ Cat ∃𝑑 ∈ Cat ∃𝑒 ∈ Cat ∃𝑧((1st ‘(⟨𝑐, 𝑑⟩ ∘F 𝑒))(((𝑑 FuncCat 𝑒) ×c (𝑐 FuncCat 𝑑)) Func (𝑐 FuncCat 𝑒))𝑧 ∧ 𝑧 ≠ (2nd ‘(⟨𝑐, 𝑑⟩ ∘F 𝑒)))
21.53.17  Kan extensions and related concepts
21.53.17.1  Kan extensions
Syntax	clan 50991	Class function defining the (local) left Kan extension.
class Lan
Syntax	cran 50992	Class function defining the (local) right Kan extension.
class Ran
Definition	df-lan 50993*	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 51013). 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 51013 (retrieved 3 Nov 2025). A left Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (lanrcl4 51020) and the second component is a natural transformation 𝐴:𝑋⟶𝐿𝐹 (lanrcl5 51021) 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 50994 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 50994*	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 51016). 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 51016 (retrieved 3 Nov 2025). A right Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (ranrcl4 51025) and the second component is a natural transformation 𝐴:𝐿𝐹⟶𝑋 (ranrcl5 51026) 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 50993 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 50995	Lan is a function on ((V × V) × V). (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Lan Fn ((V × V) × V)
Theorem	ranfn 50996	Ran is a function on ((V × V) × V). (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Ran Fn ((V × V) × V)
Theorem	reldmlan 50997	The domain of Lan is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom Lan
Theorem	reldmran 50998	The domain of Ran is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom Ran
Theorem	lanfval 50999*	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 51000*	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 𝑃)𝑥)))