P. 497 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49601-49700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oppc2ndf 49601	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 49602	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 49603	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 49604	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 49605	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 49606	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 49607	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 49608	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 49609	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 49610	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 49611*	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 49612*	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 49613	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 49614	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 49615	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 49616*	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 49617*	The constant functor of 𝑋. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝐵 × {𝑋}), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ ((𝑦𝐽𝑧) × {( 1 ‘𝑋)}))⟩)
Theorem	diag1f1lem 49618	The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. Note that (𝜑 → (𝑀 = 𝑁 ↔ 𝑋 = 𝑌)) also holds because of diag1f1 49619 and f1fveq 7210. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑀 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝑁 = ((1st ‘𝐿)‘𝑌)    ⇒   ⊢ (𝜑 → (𝑀 = 𝑁 → 𝑋 = 𝑌))
Theorem	diag1f1 49619	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 49620	Lemma for diag2f1 49621. The converse is trivial (fveq2 6835). (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = ((𝑋(2nd ‘𝐿)𝑌)‘𝐺) → 𝐹 = 𝐺))
Theorem	diag2f1 49621	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 49622	Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))    &   ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜏)) → 𝜂)    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜂) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜂) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜂))
Theorem	fucofulem2 49623*	Lemma for proving functor theorems. Maybe consider eufnfv 7177 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 49624	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩ ∈ (𝑆 × 𝑅) ↔ (𝐾𝑆𝐿 ∧ 𝐹𝑅𝐺))
Theorem	fuco2eld 49625	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝐾𝑆𝐿)    &   ⊢ (𝜑 → 𝐹𝑅𝐺)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑊)
Theorem	fuco2eld2 49626	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝑈 = ⟨⟨(1st ‘(1st ‘𝑈)), (2nd ‘(1st ‘𝑈))⟩, ⟨(1st ‘(2nd ‘𝑈)), (2nd ‘(2nd ‘𝑈))⟩⟩)
Theorem	fuco2eld3 49627	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → ((1st ‘(1st ‘𝑈))𝑆(2nd ‘(1st ‘𝑈)) ∧ (1st ‘(2nd ‘𝑈))𝑅(2nd ‘(2nd ‘𝑈))))
Syntax	cfuco 49628	Extend class notation with functor composition bifunctors.
class ∘F
Definition	df-fuco 49629*	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 49671). The object part maps two functors to their composition (fuco11 49638 and fuco11b 49649). The morphism part defines the "composition" of two natural transformations (fuco22 49651) into another natural transformation (fuco22nat 49658) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49664). Note that such "composition" is different from fucco 17893 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 49630*	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 49631*	Value of the function giving the functor composition bifunctor. Hypotheses fucofval.c and fucofval.d are not redundant (fucofvalne 49637). (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 49632	A functor composition bifunctor is an ordered pair. Enables 1st2ndb 7975. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    ⇒   ⊢ (𝜑 → ⚬ ∈ (V × V))
Theorem	fuco1 49633	The object part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑂 = ( ∘func ↾ 𝑊))
Theorem	fucof1 49634	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 49635*	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 49636	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 49637*	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 49638	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 49639	The object part of the functor composition bifunctor maps into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) ∈ (𝐶 Func 𝐸))
Theorem	fuco11a 49640*	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 49641*	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 49642	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 49643	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 49644	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 49645	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 49646	The identity morphism of the mapped object. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑂‘𝑈)) = ( 1 ∘ (𝐾 ∘ 𝐹)))
Theorem	fuco11idx 49647	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 49648*	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 49649	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 49650	Alternate proof of fuco11b 49649. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑂)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺𝑂𝐹) = (𝐺 ∘func 𝐹))
Theorem	fuco22 49651*	The morphism part of the functor composition bifunctor. See also fuco22a 49662. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝐴‘𝑥)))))
Theorem	fucofn22 49652	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 49653	The morphism part of the functor composition bifunctor. See also fuco23a 49664. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋))))    ⇒   ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((𝐵‘(𝑀‘𝑋)) ∗ (((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))))
Theorem	fuco22natlem1 49654	Lemma for fuco22nat 49658. 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 49655	Lemma for fuco22nat 49658. The commutative square of natural transformation 𝐵 in category 𝐸, combined with the commutative square of fuco22natlem1 49654. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (((𝐵‘(𝑀‘𝑌))(⟨(𝐾‘(𝐹‘𝑌)), (𝐾‘(𝑀‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌)))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝑆(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋)))))
Theorem	fuco22natlem3 49656	Combine fuco22natlem2 49655 with fuco23 49653. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (((𝐵(𝑈𝑃𝑉)𝐴)‘𝑌)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝐾 ∘ 𝐹)‘𝑌)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((((𝐹‘𝑋)𝐿(𝐹‘𝑌)) ∘ (𝑋𝐺𝑌))‘𝐻)) = (((((𝑀‘𝑋)𝑆(𝑀‘𝑌)) ∘ (𝑋𝑁𝑌))‘𝐻)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝑅 ∘ 𝑀)‘𝑋)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋)))
Theorem	fuco22natlem 49657	The composed natural transformation is a natural transformation. Use fuco22nat 49658 instead. (New usage is discouraged.) (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fuco22nat 49658	The composed natural transformation is a natural transformation. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅))    &   ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩)    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fucof21 49659	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 49660	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid2 49661. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈)))
Theorem	fucoid2 49661	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid 49660. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈)))
Theorem	fuco22a 49662*	The morphism part of the functor composition bifunctor. See also fuco22 49651. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘((1st ‘𝑀)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑀)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑅)‘((1st ‘𝑀)‘𝑥)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐾)((1st ‘𝑀)‘𝑥))‘(𝐴‘𝑥)))))
Theorem	fuco23alem 49663	The naturality property (nati 17886) in category 𝐸. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ · = (comp‘𝐸)    ⇒   ⊢ (𝜑 → ((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(𝐵‘(𝐹‘𝑋))))
Theorem	fuco23a 49664	The morphism part of the functor composition bifunctor. An alternate definition of ∘F. See also fuco23 49653. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋))))    ⇒   ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋)) ∗ (𝐵‘(𝐹‘𝑋))))
Theorem	fucocolem1 49665	Lemma for fucoco 49669. 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 49666*	Lemma for fucoco 49669. 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 49667*	Lemma for fucoco 49669. 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 49668*	Lemma for fucoco 49669. 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 49669	Composition in the source category is mapped to composition in the target. See also fucoco2 49670. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ · = (comp‘𝑇)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))
Theorem	fucoco2 49670	Composition in the source category is mapped to composition in the target. See also fucoco 49669. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ · = (comp‘𝑇)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐽𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))
Theorem	fucofunc 49671	The functor composition bifunctor is a functor. See also fucofunca 49672. 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 49785), for example, (SetCat‘1o) (the trivial category, setc1oterm 49803), 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 49653. 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 49629 up to fuco23 49653, but ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) might be mapped to a different morphism in category 𝐸. See fucofulem2 49623 for some insights. 2. fuco22nat 49658, fucoid 49660, and fucoco 49669 are satisfied. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑂(𝑇 Func 𝑄)𝑃)
Theorem	fucofunca 49672	The functor composition bifunctor is a functor. See also fucofunc 49671. (Contributed by Zhi Wang, 10-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) ∈ (𝑇 Func 𝑄))
Theorem	fucolid 49673*	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 49674*	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 49675	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 49676*	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 49677	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 49678	Lemma for precofval 49679 to enable catlid 17610 or catrid 17611. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((((𝐹‘𝑋)𝐿(𝐹‘𝑋))‘(( 1 ∘ 𝐹)‘𝑋)) = (𝐼‘(𝐾‘(𝐹‘𝑋))) ∧ (𝐾‘(𝐹‘𝑋)) ∈ 𝐵))
Theorem	precofval 49679*	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 49680*	Alternate proof of precofval 49679. (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 49681*	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 49682	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 49683*	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 49684*	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 49685	Extend class notation with pre-composition functors.
class −∘F
Definition	df-prcof 49686*	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 49683). But such definition requires an explicit third category. prcoftposcurfuco 49695 and prcoftposcurfucoa 49696 prove the equivalence. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ −∘F = (𝑝 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩)
Theorem	reldmprcof 49687	The domain of −∘F is a relation. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ Rel dom −∘F
Theorem	prcofvalg 49688*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑉)    &   ⊢ (𝜑 → (1st ‘𝑃) = 𝐷)    &   ⊢ (𝜑 → (2nd ‘𝑃) = 𝐸)    ⇒   ⊢ (𝜑 → (𝑃 −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩)
Theorem	prcofvala 49689*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩)
Theorem	prcofval 49690*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ Rel 𝑅    &   ⊢ (𝜑 → 𝐹𝑅𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func ⟨𝐹, 𝐺⟩)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ 𝐹)))⟩)
Theorem	prcofpropd 49691	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 𝐹))
Theorem	prcofelvv 49692	The pre-composition functor is an ordered pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑃 −∘F 𝐹) ∈ (V × V))
Theorem	reldmprcof1 49693	The domain of the object part of the pre-composition functor is a relation. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ Rel dom (1st ‘(𝑃 −∘F 𝐹))
Theorem	reldmprcof2 49694	The domain of the morphism part of the pre-composition functor is a relation. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ Rel dom (2nd ‘(𝑃 −∘F 𝐹))
Theorem	prcoftposcurfuco 49695	The pre-composition functor is the transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅))))    &   ⊢ (𝜑 → 𝑀 = ((1st ‘ ⚬ )‘⟨𝐹, 𝐺⟩))    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) = 𝑀)
Theorem	prcoftposcurfucoa 49696	The pre-composition functor is the transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄 swapF 𝑅))))    &   ⊢ (𝜑 → 𝑀 = ((1st ‘ ⚬ )‘𝐹))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = 𝑀)
Theorem	prcoffunc 49697	The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) ∈ (𝑅 Func 𝑆))
Theorem	prcoffunca 49698	The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) ∈ (𝑅 Func 𝑆))
Theorem	prcoffunca2 49699	The pre-composition functor is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐾, 𝐿⟩)    ⇒   ⊢ (𝜑 → 𝐾(𝑅 Func 𝑆)𝐿)
Theorem	prcof1 49700	The object part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → (1st ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑂)    ⇒   ⊢ (𝜑 → (𝑂‘𝐾) = (𝐾 ∘func 𝐹))