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	swapfida 49901	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfid 49900. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 1 = (Id‘𝑆)    &   ⊢ 𝐼 = (Id‘𝑇)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝑂‘𝑋)))
Theorem	swapfcoa 49902	Composition in the source category is mapped to composition in the target. (𝜑 → 𝐶 ∈ Cat) and (𝜑 → 𝐷 ∈ Cat) can be replaced by a weaker hypothesis (𝜑 → 𝑆 ∈ Cat). (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝑆)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑍))    &   ⊢ · = (comp‘𝑆)    &   ⊢ ∙ = (comp‘𝑇)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝑁(⟨𝑋, 𝑌⟩ · 𝑍)𝑀)) = (((𝑌𝑃𝑍)‘𝑁)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝑀)))
Theorem	swapffunc 49903	The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑂(𝑆 Func 𝑇)𝑃)
Theorem	swapfffth 49904	The swap functor is a fully faithful functor. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑂((𝑆 Full 𝑇) ∩ (𝑆 Faith 𝑇))𝑃)
Theorem	swapffunca 49905	The swap functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (𝑆 Func 𝑇))
Theorem	swapfiso 49906	The swap functor is an isomorphism between product categories. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    &   ⊢ 𝐼 = (Iso‘𝐸)    ⇒   ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (𝑆𝐼𝑇))
Theorem	swapciso 49907	The product category is categorically isomorphic to the swapped product category. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑆( ≃𝑐 ‘𝐸)𝑇)
21.49.15.15  Functor evaluation
Theorem	oppc1stflem 49908*	A utility theorem for proving theorems on projection functors of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) → ( oppFunc ‘(𝐶𝐹𝐷)) = (𝑂𝐹𝑃))    &   ⊢ 𝐹 = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ 𝑌)    ⇒   ⊢ (𝜑 → ( oppFunc ‘(𝐶𝐹𝐷)) = (𝑂𝐹𝑃))
Theorem	oppc1stf 49909	The opposite functor of the first projection functor is the first projection functor of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( oppFunc ‘(𝐶 1stF 𝐷)) = (𝑂 1stF 𝑃))
Theorem	oppc2ndf 49910	The opposite functor of the second projection functor is the second projection functor of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( oppFunc ‘(𝐶 2ndF 𝐷)) = (𝑂 2ndF 𝑃))
Theorem	1stfpropd 49911	If two categories have the same set of objects, morphisms, and compositions, then they have same first projection functors. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ Cat)    &   ⊢ (𝜑 → 𝐵 ∈ Cat)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (𝐴 1stF 𝐶) = (𝐵 1stF 𝐷))
Theorem	2ndfpropd 49912	If two categories have the same set of objects, morphisms, and compositions, then they have same second projection functors. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ Cat)    &   ⊢ (𝜑 → 𝐵 ∈ Cat)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (𝐴 2ndF 𝐶) = (𝐵 2ndF 𝐷))
Theorem	diagpropd 49913	If two categories have the same set of objects, morphisms, and compositions, then they have same diagonal functors. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ Cat)    &   ⊢ (𝜑 → 𝐵 ∈ Cat)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (𝐴Δfunc𝐶) = (𝐵Δfunc𝐷))
21.49.15.16  Transposed curry functors
Theorem	cofuswapfcl 49914	The bifunctor pre-composed with a swap functor is a bifunctor. (Contributed by Zhi Wang, 10-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ (𝜑 → 𝐺 = (𝐹 ∘func (𝐶 swapF 𝐷)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
Theorem	cofuswapf1 49915	The object part of a bifunctor pre-composed with a swap functor. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ (𝜑 → 𝐺 = (𝐹 ∘func (𝐶 swapF 𝐷)))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(1st ‘𝐺)𝑌) = (𝑌(1st ‘𝐹)𝑋))
Theorem	cofuswapf2 49916	The morphism part of a bifunctor pre-composed with a swap functor. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ (𝜑 → 𝐺 = (𝐹 ∘func (𝐶 swapF 𝐷)))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑍))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐽𝑊))    ⇒   ⊢ (𝜑 → (𝑀(⟨𝑋, 𝑌⟩(2nd ‘𝐺)⟨𝑍, 𝑊⟩)𝑁) = (𝑁(⟨𝑌, 𝑋⟩(2nd ‘𝐹)⟨𝑊, 𝑍⟩)𝑀))
Theorem	tposcurf1cl 49917	The partially evaluated transposed curry functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷))))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘𝐺)‘𝑋))    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))
Theorem	tposcurf11 49918	Value of the double evaluated transposed curry functor. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷))))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘𝐺)‘𝑋))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑌) = (𝑌(1st ‘𝐹)𝑋))
Theorem	tposcurf12 49919	The partially evaluated transposed curry functor at a morphism. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷))))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘𝐺)‘𝑋))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐻) = (𝐻(⟨𝑌, 𝑋⟩(2nd ‘𝐹)⟨𝑍, 𝑋⟩)( 1 ‘𝑋)))
Theorem	tposcurf1 49920*	Value of the object part of the transposed curry functor. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷))))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘𝐺)‘𝑋))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑦(1st ‘𝐹)𝑋)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (𝑔(⟨𝑦, 𝑋⟩(2nd ‘𝐹)⟨𝑧, 𝑋⟩)( 1 ‘𝑋))))⟩)
Theorem	tposcurf2 49921*	Value of the transposed curry functor at a morphism. (Contributed by Zhi Wang, 10-Oct-2025.)
⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷))))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾))    ⇒   ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ ((𝐼‘𝑧)(⟨𝑧, 𝑋⟩(2nd ‘𝐹)⟨𝑧, 𝑌⟩)𝐾)))
Theorem	tposcurf2val 49922	Value of a component of the transposed curry functor natural transformation. (Contributed by Zhi Wang, 10-Oct-2025.)
⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷))))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐿‘𝑍) = ((𝐼‘𝑍)(⟨𝑍, 𝑋⟩(2nd ‘𝐹)⟨𝑍, 𝑌⟩)𝐾))
Theorem	tposcurf2cl 49923	The transposed curry functor at a morphism is a natural transformation. (Contributed by Zhi Wang, 10-Oct-2025.)
⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷))))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾))    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌)))
Theorem	tposcurfcl 49924	The transposed curry functor of a functor 𝐹:𝐷 × 𝐶⟶𝐸 is a functor tposcurry (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐺 = (⟨𝐶, 𝐷⟩ curryF (𝐹 ∘func (𝐶 swapF 𝐷))))    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐷 ×c 𝐶) Func 𝐸))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝑄))
21.49.15.17  Constant functors
Theorem	diag1 49925*	The constant functor of 𝑋. Example 3.20(2) of [Adamek] p. 30. (Contributed by Zhi Wang, 17-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ 𝑋), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑓 ∈ (𝑦𝐽𝑧) ↦ ( 1 ‘𝑋)))⟩)
Theorem	diag1a 49926*	The constant functor of 𝑋. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝐵 × {𝑋}), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ ((𝑦𝐽𝑧) × {( 1 ‘𝑋)}))⟩)
Theorem	diag1f1lem 49927	The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. Note that (𝜑 → (𝑀 = 𝑁 ↔ 𝑋 = 𝑌)) also holds because of diag1f1 49928 and f1fveq 7246. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑀 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝑁 = ((1st ‘𝐿)‘𝑌)    ⇒   ⊢ (𝜑 → (𝑀 = 𝑁 → 𝑋 = 𝑌))
Theorem	diag1f1 49928	The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → (1st ‘𝐿):𝐴–1-1→(𝐷 Func 𝐶))
Theorem	diag2f1lem 49929	Lemma for diag2f1 49930. The converse is trivial (fveq2 6867). (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = ((𝑋(2nd ‘𝐿)𝑌)‘𝐺) → 𝐹 = 𝐺))
Theorem	diag2f1 49930	If 𝐵 is non-empty, the morphism part of a diagonal functor is injective functions from hom-sets into sets of natural transformations. (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝐿)𝑌):(𝑋𝐻𝑌)–1-1→(((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌)))
21.49.15.18  Functor composition bifunctors
Theorem	fucofulem1 49931	Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))    &   ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜏)) → 𝜂)    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜂) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜂) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜂))
Theorem	fucofulem2 49932*	Lemma for proving functor theorems. Maybe consider eufnfv 7213 to prove the uniqueness of a functor. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐵 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))    &   ⊢ 𝐻 = (Hom ‘((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷)))    ⇒   ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(𝐶 Nat 𝐸)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑢𝐺𝑣)) ∧ ∀𝑚 ∈ 𝐵 ∀𝑛 ∈ 𝐵 ((𝑚𝐺𝑛) = (𝑏 ∈ ((1st ‘𝑚)(𝐷 Nat 𝐸)(1st ‘𝑛)), 𝑎 ∈ ((2nd ‘𝑚)(𝐶 Nat 𝐷)(2nd ‘𝑛)) ↦ (𝑏(𝑚𝐺𝑛)𝑎)) ∧ ∀𝑝 ∈ ((1st ‘𝑚)(𝐷 Nat 𝐸)(1st ‘𝑛))∀𝑞 ∈ ((2nd ‘𝑚)(𝐶 Nat 𝐷)(2nd ‘𝑛))(𝑝(𝑚𝐺𝑛)𝑞) ∈ ((𝐹‘𝑚)(𝐶 Nat 𝐸)(𝐹‘𝑛)))))
Theorem	fuco2el 49933	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩ ∈ (𝑆 × 𝑅) ↔ (𝐾𝑆𝐿 ∧ 𝐹𝑅𝐺))
Theorem	fuco2eld 49934	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝐾𝑆𝐿)    &   ⊢ (𝜑 → 𝐹𝑅𝐺)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑊)
Theorem	fuco2eld2 49935	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝑈 = ⟨⟨(1st ‘(1st ‘𝑈)), (2nd ‘(1st ‘𝑈))⟩, ⟨(1st ‘(2nd ‘𝑈)), (2nd ‘(2nd ‘𝑈))⟩⟩)
Theorem	fuco2eld3 49936	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → ((1st ‘(1st ‘𝑈))𝑆(2nd ‘(1st ‘𝑈)) ∧ (1st ‘(2nd ‘𝑈))𝑅(2nd ‘(2nd ‘𝑈))))
Syntax	cfuco 49937	Extend class notation with functor composition bifunctors.
class ∘F
Definition	df-fuco 49938*	Definition of functor composition bifunctors. Given three categories 𝐶, 𝐷, and 𝐸, (⟨𝐶, 𝐷⟩ ∘F 𝐸) is a functor from the product category of two categories of functors to a category of functors (fucofunc 49980). The object part maps two functors to their composition (fuco11 49947 and fuco11b 49958). The morphism part defines the "composition" of two natural transformations (fuco22 49960) into another natural transformation (fuco22nat 49967) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49973). Note that such "composition" is different from fucco 17998 because they "compose" along different "axes". (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ ∘F = (𝑝 ∈ V, 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝑑 Nat 𝑒)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝑐 Nat 𝑑)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
Theorem	fucofvalg 49939*	Value of the function giving the functor composition bifunctor. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝑃 ∈ 𝑈)    &   ⊢ (𝜑 → (1st ‘𝑃) = 𝐶)    &   ⊢ (𝜑 → (2nd ‘𝑃) = 𝐷)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑃 ∘F 𝐸) = ⚬ )    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → ⚬ = ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
Theorem	fucofval 49940*	Value of the function giving the functor composition bifunctor. Hypotheses fucofval.c and fucofval.d are not redundant (fucofvalne 49946). (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → ⚬ = ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
Theorem	fucoelvv 49941	A functor composition bifunctor is an ordered pair. Enables 1st2ndb 8010. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    ⇒   ⊢ (𝜑 → ⚬ ∈ (V × V))
Theorem	fuco1 49942	The object part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑂 = ( ∘func ↾ 𝑊))
Theorem	fucof1 49943	The object part of the functor composition bifunctor maps ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑂:𝑊⟶(𝐶 Func 𝐸))
Theorem	fuco2 49944*	The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑃 = (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))))
Theorem	fucofn2 49945	The morphism part of the functor composition bifunctor is a function on the Cartesian square of the base set. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑃 Fn (𝑊 × 𝑊))
Theorem	fucofvalne 49946*	Value of the function giving the functor composition bifunctor, if 𝐶 or 𝐷 are not sets. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → ¬ (𝐶 ∈ V ∧ 𝐷 ∈ V))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → ⚬ ≠ ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
Theorem	fuco11 49947	The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) = (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩))
Theorem	fuco11cl 49948	The object part of the functor composition bifunctor maps into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) ∈ (𝐶 Func 𝐸))
Theorem	fuco11a 49949*	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) = ⟨(𝐾 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐿(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))⟩)
Theorem	fuco112 49950*	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (2nd ‘(𝑂‘𝑈)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐿(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦))))
Theorem	fuco111 49951	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (1st ‘(𝑂‘𝑈)) = (𝐾 ∘ 𝐹))
Theorem	fuco111x 49952	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. An object is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → ((1st ‘(𝑂‘𝑈))‘𝑋) = (𝐾‘(𝐹‘𝑋)))
Theorem	fuco112x 49953	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘(𝑂‘𝑈))𝑌) = (((𝐹‘𝑋)𝐿(𝐹‘𝑌)) ∘ (𝑋𝐺𝑌)))
Theorem	fuco112xa 49954	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. A morphism is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋(Hom ‘𝐶)𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘(𝑂‘𝑈))𝑌)‘𝐴) = (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐴)))
Theorem	fuco11id 49955	The identity morphism of the mapped object. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑂‘𝑈)) = ( 1 ∘ (𝐾 ∘ 𝐹)))
Theorem	fuco11idx 49956	The identity morphism of the mapped object. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → ((𝐼‘(𝑂‘𝑈))‘𝑋) = ( 1 ‘(𝐾‘(𝐹‘𝑋))))
Theorem	fuco21 49957*	The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑀(𝐶 Func 𝐷)𝑁)    &   ⊢ (𝜑 → 𝑅(𝐷 Func 𝐸)𝑆)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (𝑈𝑃𝑉) = (𝑏 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩), 𝑎 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝑎‘𝑥))))))
Theorem	fuco11b 49958	The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑂)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺𝑂𝐹) = (𝐺 ∘func 𝐹))
Theorem	fuco11bALT 49959	Alternate proof of fuco11b 49958. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑂)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺𝑂𝐹) = (𝐺 ∘func 𝐹))
Theorem	fuco22 49960*	The morphism part of the functor composition bifunctor. See also fuco22a 49971. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝐴‘𝑥)))))
Theorem	fucofn22 49961	The morphism part of the functor composition bifunctor maps two natural transformations to a function on a base set. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) Fn (Base‘𝐶))
Theorem	fuco23 49962	The morphism part of the functor composition bifunctor. See also fuco23a 49973. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋))))    ⇒   ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((𝐵‘(𝑀‘𝑋)) ∗ (((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))))
Theorem	fuco22natlem1 49963	Lemma for fuco22nat 49967. The commutative square of natural transformation 𝐴 in category 𝐷, mapped to category 𝐸 by the morphism part 𝐿 of the functor. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    ⇒   ⊢ (𝜑 → ((((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝐾‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝐿(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝐾‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))))
Theorem	fuco22natlem2 49964	Lemma for fuco22nat 49967. The commutative square of natural transformation 𝐵 in category 𝐸, combined with the commutative square of fuco22natlem1 49963. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (((𝐵‘(𝑀‘𝑌))(⟨(𝐾‘(𝐹‘𝑌)), (𝐾‘(𝑀‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌)))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝑆(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋)))))
Theorem	fuco22natlem3 49965	Combine fuco22natlem2 49964 with fuco23 49962. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (((𝐵(𝑈𝑃𝑉)𝐴)‘𝑌)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝐾 ∘ 𝐹)‘𝑌)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((((𝐹‘𝑋)𝐿(𝐹‘𝑌)) ∘ (𝑋𝐺𝑌))‘𝐻)) = (((((𝑀‘𝑋)𝑆(𝑀‘𝑌)) ∘ (𝑋𝑁𝑌))‘𝐻)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝑅 ∘ 𝑀)‘𝑋)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋)))
Theorem	fuco22natlem 49966	The composed natural transformation is a natural transformation. Use fuco22nat 49967 instead. (New usage is discouraged.) (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fuco22nat 49967	The composed natural transformation is a natural transformation. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅))    &   ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩)    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fucof21 49968	The morphism part of the functor composition bifunctor maps a hom-set of the product category into a set of natural transformations. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑈𝑃𝑉):(𝑈𝐽𝑉)⟶((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fucoid 49969	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid2 49970. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈)))
Theorem	fucoid2 49970	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid 49969. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈)))
Theorem	fuco22a 49971*	The morphism part of the functor composition bifunctor. See also fuco22 49960. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘((1st ‘𝑀)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑀)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑅)‘((1st ‘𝑀)‘𝑥)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐾)((1st ‘𝑀)‘𝑥))‘(𝐴‘𝑥)))))
Theorem	fuco23alem 49972	The naturality property (nati 17991) in category 𝐸. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ · = (comp‘𝐸)    ⇒   ⊢ (𝜑 → ((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(𝐵‘(𝐹‘𝑋))))
Theorem	fuco23a 49973	The morphism part of the functor composition bifunctor. An alternate definition of ∘F. See also fuco23 49962. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋))))    ⇒   ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋)) ∗ (𝐵‘(𝐹‘𝑋))))
Theorem	fucocolem1 49974	Lemma for fucoco 49978. Associativity for morphisms in category 𝐸. To simply put, ((𝑎 · 𝑏) · (𝑐 · 𝑑)) = (𝑎 · ((𝑏 · 𝑐) · 𝑑)) for morphism compositions. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ (((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))(Hom ‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋))))    &   ⊢ (𝜑 → 𝐵 ∈ (((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))(Hom ‘𝐸)((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))))    ⇒   ⊢ (𝜑 → (((𝑈‘((1st ‘𝑁)‘𝑋))(⟨((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))𝐴)(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))(𝐵(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋)))((((1st ‘𝐺)‘𝑋)(2nd ‘𝐹)((1st ‘𝐿)‘𝑋))‘(𝑆‘𝑋)))) = ((𝑈‘((1st ‘𝑁)‘𝑋))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))((𝐴(⟨((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋)), ((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋)))𝐵)(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋)))((((1st ‘𝐺)‘𝑋)(2nd ‘𝐹)((1st ‘𝐿)‘𝑋))‘(𝑆‘𝑋)))))
Theorem	fucocolem2 49975*	Lemma for fucoco 49978. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ · = (comp‘𝑇)    &   ⊢ ∗ = (comp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))(𝑅‘((1st ‘𝑁)‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝑁)‘𝑥))‘((𝑉‘𝑥)(⟨((1st ‘𝐺)‘𝑥), ((1st ‘𝐿)‘𝑥)⟩ ∗ ((1st ‘𝑁)‘𝑥))(𝑆‘𝑥))))))
Theorem	fucocolem3 49976*	Lemma for fucoco 49978. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ · = (comp‘𝑇)    &   ⊢ ∗ = (comp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))(((𝑅‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐹)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))))))
Theorem	fucocolem4 49977*	Lemma for fucoco 49978. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ ∙ = (comp‘𝑄)    ⇒   ⊢ (𝜑 → (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))))))
Theorem	fucoco 49978	Composition in the source category is mapped to composition in the target. See also fucoco2 49979. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ · = (comp‘𝑇)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))
Theorem	fucoco2 49979	Composition in the source category is mapped to composition in the target. See also fucoco 49978. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ · = (comp‘𝑇)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐽𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))
Theorem	fucofunc 49980	The functor composition bifunctor is a functor. See also fucofunca 49981. However, it is unlikely the unique functor compatible with the functor composition. As a counterexample, let 𝐶 and 𝐷 be terminal categories (categories of one object and one morphism, df-termc 50094), for example, (SetCat‘1o) (the trivial category, setc1oterm 50112), and 𝐸 be a category with two objects equipped with only two non-identity morphisms 𝑓 and 𝑔, pointing in the same direction. It is possible to map the ordered pair of natural transformations ⟨𝑎, 𝑖⟩, where 𝑎 sends to 𝑓 and 𝑖 is the identity natural transformation, to the other natural transformation 𝑏 sending to 𝑔, i.e., define the morphism part 𝑃 such that (𝑎(𝑈𝑃𝑉)𝑖) = 𝑏 such that (𝑏‘𝑋) = 𝑔 given hypotheses of fuco23 49962. Such construction should be provable as a functor. Given any 𝑃, it is a morphism part of a functor compatible with the object part, i.e., the functor composition, i.e., the restriction of ∘func, iff both of the following hold. 1. It has the same form as df-fuco 49938 up to fuco23 49962, but ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) might be mapped to a different morphism in category 𝐸. See fucofulem2 49932 for some insights. 2. fuco22nat 49967, fucoid 49969, and fucoco 49978 are satisfied. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑂(𝑇 Func 𝑄)𝑃)
Theorem	fucofunca 49981	The functor composition bifunctor is a functor. See also fucofunc 49980. (Contributed by Zhi Wang, 10-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) ∈ (𝑇 Func 𝑄))
Theorem	fucolid 49982*	Post-compose a natural transformation with an identity natural transformation. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐶 Nat 𝐷)𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐼‘𝐹)(⟨𝐹, 𝐺⟩𝑃⟨𝐹, 𝐻⟩)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐻)‘𝑥))‘(𝐴‘𝑥))))
Theorem	fucorid 49983*	Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor, in maps-to notation. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐷 Nat 𝐸)𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐴(⟨𝐺, 𝐹⟩𝑃⟨𝐻, 𝐹⟩)(𝐼‘𝐹)) = (𝑥 ∈ (Base‘𝐶) ↦ (𝐴‘((1st ‘𝐹)‘𝑥))))
Theorem	fucorid2 49984	Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐷 Nat 𝐸)𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐴(⟨𝐺, 𝐹⟩𝑃⟨𝐻, 𝐹⟩)(𝐼‘𝐹)) = (𝐴 ∘ (1st ‘𝐹)))
21.49.15.19  Post-composition functors
Theorem	postcofval 49985*	Value of the post-composition functor as a curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐷⟩ ∘F 𝐸))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝐹)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐶 Func 𝐷) ↦ (𝐹 ∘func 𝑔)), (𝑔 ∈ (𝐶 Func 𝐷), ℎ ∈ (𝐶 Func 𝐷) ↦ (𝑎 ∈ (𝑔(𝐶 Nat 𝐷)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((((1st ‘𝑔)‘𝑥)(2nd ‘𝐹)((1st ‘ℎ)‘𝑥))‘(𝑎‘𝑥)))))⟩)
Theorem	postcofcl 49986	The post-composition functor as a curry of the functor composition bifunctor is a functor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐷⟩ ∘F 𝐸))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝐹)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑄 Func 𝑆))
21.49.15.20  Pre-composition functors
Theorem	precofvallem 49987	Lemma for precofval 49988 to enable catlid 17715 or catrid 17716. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((((𝐹‘𝑋)𝐿(𝐹‘𝑋))‘(( 1 ∘ 𝐹)‘𝑋)) = (𝐼‘(𝐾‘(𝐹‘𝑋))) ∧ (𝐾‘(𝐹‘𝑋)) ∈ 𝐵))
Theorem	precofval 49988*	Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅))))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹))    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ (𝑎‘((1st ‘𝐹)‘𝑥)))))⟩)
Theorem	precofvalALT 49989*	Alternate proof of precofval 49988. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅))))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹))    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ (𝑎‘((1st ‘𝐹)‘𝑥)))))⟩)
Theorem	precofval2 49990*	Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅))))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹))    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩)
Theorem	precofcl 49991	The pre-composition functor as a transposed curry of the functor composition bifunctor is a functor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅))))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹))    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑅 Func 𝑆))
Theorem	precofval3 49992*	Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = (𝑔 ∈ 𝐵 ↦ (𝑔 ∘func ⟨𝐹, 𝐺⟩)))    &   ⊢ (𝜑 → 𝐿 = (𝑔 ∈ 𝐵, ℎ ∈ 𝐵 ↦ (𝑎 ∈ (𝑔𝑁ℎ) ↦ (𝑎 ∘ 𝐹))))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅))))    &   ⊢ (𝜑 → 𝑀 = ((1st ‘ ⚬ )‘⟨𝐹, 𝐺⟩))    ⇒   ⊢ (𝜑 → ⟨𝐾, 𝐿⟩ = 𝑀)
Theorem	precoffunc 49993*	The pre-composition functor, expressed explicitly, is a functor. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof shortened by Zhi Wang, 20-Oct-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = (𝑔 ∈ 𝐵 ↦ (𝑔 ∘func ⟨𝐹, 𝐺⟩)))    &   ⊢ (𝜑 → 𝐿 = (𝑔 ∈ 𝐵, ℎ ∈ 𝐵 ↦ (𝑎 ∈ (𝑔𝑁ℎ) ↦ (𝑎 ∘ 𝐹))))    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    ⇒   ⊢ (𝜑 → 𝐾(𝑅 Func 𝑆)𝐿)
Syntax	cprcof 49994	Extend class notation with pre-composition functors.
class −∘F
Definition	df-prcof 49995*	Definition of pre-composition functors. The object part of the pre-composition functor given by 𝐹 pre-composes a functor with 𝐹; the morphism part pre-composes a natural transformation with the object part of 𝐹, in terms of function composition. Comments before 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 (retrieved 3 Nov 2025). The notation −∘F is inspired by this page: https://1lab.dev/Cat.Functor.Compose.html. The pre-composition functor can also be defined as a transposed curry of the functor composition bifunctor (precofval3 49992). But such definition requires an explicit third category. prcoftposcurfuco 50004 and prcoftposcurfucoa 50005 prove the equivalence. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ −∘F = (𝑝 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩)
Theorem	reldmprcof 49996	The domain of −∘F is a relation. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ Rel dom −∘F
Theorem	prcofvalg 49997*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑉)    &   ⊢ (𝜑 → (1st ‘𝑃) = 𝐷)    &   ⊢ (𝜑 → (2nd ‘𝑃) = 𝐸)    ⇒   ⊢ (𝜑 → (𝑃 −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩)
Theorem	prcofvala 49998*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩)
Theorem	prcofval 49999*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ Rel 𝑅    &   ⊢ (𝜑 → 𝐹𝑅𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func ⟨𝐹, 𝐺⟩)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ 𝐹)))⟩)
Theorem	prcofpropd 50000	If the categories have the same set of objects, morphisms, and compositions, then they have the same pre-composition functors. (Contributed by Zhi Wang, 21-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐶⟩ −∘F 𝐹) = (⟨𝐵, 𝐷⟩ −∘F 𝐹))