P. 495 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49401-49500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	1stfpropd 49401	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 49402	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 49403	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 49404	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 49405	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 49406	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 49407	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 49408	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 49409	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 49410*	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 49411*	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 49412	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 49413	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 49414	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 49415*	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 49416*	The constant functor of 𝑋. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝐵 × {𝑋}), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ ((𝑦𝐽𝑧) × {( 1 ‘𝑋)}))⟩)
Theorem	diag1f1lem 49417	The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. Note that (𝜑 → (𝑀 = 𝑁 ↔ 𝑋 = 𝑌)) also holds because of diag1f1 49418 and f1fveq 7196. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑀 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝑁 = ((1st ‘𝐿)‘𝑌)    ⇒   ⊢ (𝜑 → (𝑀 = 𝑁 → 𝑋 = 𝑌))
Theorem	diag1f1 49418	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 49419	Lemma for diag2f1 49420. The converse is trivial (fveq2 6822). (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = ((𝑋(2nd ‘𝐿)𝑌)‘𝐺) → 𝐹 = 𝐺))
Theorem	diag2f1 49420	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 49421	Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))    &   ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜏)) → 𝜂)    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜂) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜂) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜂))
Theorem	fucofulem2 49422*	Lemma for proving functor theorems. Maybe consider eufnfv 7163 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 49423	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩ ∈ (𝑆 × 𝑅) ↔ (𝐾𝑆𝐿 ∧ 𝐹𝑅𝐺))
Theorem	fuco2eld 49424	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝐾𝑆𝐿)    &   ⊢ (𝜑 → 𝐹𝑅𝐺)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑊)
Theorem	fuco2eld2 49425	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝑈 = ⟨⟨(1st ‘(1st ‘𝑈)), (2nd ‘(1st ‘𝑈))⟩, ⟨(1st ‘(2nd ‘𝑈)), (2nd ‘(2nd ‘𝑈))⟩⟩)
Theorem	fuco2eld3 49426	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → ((1st ‘(1st ‘𝑈))𝑆(2nd ‘(1st ‘𝑈)) ∧ (1st ‘(2nd ‘𝑈))𝑅(2nd ‘(2nd ‘𝑈))))
Syntax	cfuco 49427	Extend class notation with functor composition bifunctors.
class ∘F
Definition	df-fuco 49428*	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 49470). The object part maps two functors to their composition (fuco11 49437 and fuco11b 49448). The morphism part defines the "composition" of two natural transformations (fuco22 49450) into another natural transformation (fuco22nat 49457) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49463). Note that such "composition" is different from fucco 17872 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 49429*	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 49430*	Value of the function giving the functor composition bifunctor. Hypotheses fucofval.c and fucofval.d are not redundant (fucofvalne 49436). (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 49431	A functor composition bifunctor is an ordered pair. Enables 1st2ndb 7961. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    ⇒   ⊢ (𝜑 → ⚬ ∈ (V × V))
Theorem	fuco1 49432	The object part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑂 = ( ∘func ↾ 𝑊))
Theorem	fucof1 49433	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 49434*	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 49435	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 49436*	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 49437	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 49438	The object part of the functor composition bifunctor maps into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) ∈ (𝐶 Func 𝐸))
Theorem	fuco11a 49439*	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 49440*	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 49441	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 49442	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 49443	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 49444	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 49445	The identity morphism of the mapped object. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑂‘𝑈)) = ( 1 ∘ (𝐾 ∘ 𝐹)))
Theorem	fuco11idx 49446	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 49447*	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 49448	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 49449	Alternate proof of fuco11b 49448. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑂)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺𝑂𝐹) = (𝐺 ∘func 𝐹))
Theorem	fuco22 49450*	The morphism part of the functor composition bifunctor. See also fuco22a 49461. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝐴‘𝑥)))))
Theorem	fucofn22 49451	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 49452	The morphism part of the functor composition bifunctor. See also fuco23a 49463. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋))))    ⇒   ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((𝐵‘(𝑀‘𝑋)) ∗ (((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))))
Theorem	fuco22natlem1 49453	Lemma for fuco22nat 49457. 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 49454	Lemma for fuco22nat 49457. The commutative square of natural transformation 𝐵 in category 𝐸, combined with the commutative square of fuco22natlem1 49453. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (((𝐵‘(𝑀‘𝑌))(⟨(𝐾‘(𝐹‘𝑌)), (𝐾‘(𝑀‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌)))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝑆(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋)))))
Theorem	fuco22natlem3 49455	Combine fuco22natlem2 49454 with fuco23 49452. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (((𝐵(𝑈𝑃𝑉)𝐴)‘𝑌)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝐾 ∘ 𝐹)‘𝑌)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((((𝐹‘𝑋)𝐿(𝐹‘𝑌)) ∘ (𝑋𝐺𝑌))‘𝐻)) = (((((𝑀‘𝑋)𝑆(𝑀‘𝑌)) ∘ (𝑋𝑁𝑌))‘𝐻)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝑅 ∘ 𝑀)‘𝑋)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋)))
Theorem	fuco22natlem 49456	The composed natural transformation is a natural transformation. Use fuco22nat 49457 instead. (New usage is discouraged.) (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fuco22nat 49457	The composed natural transformation is a natural transformation. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅))    &   ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩)    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fucof21 49458	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 49459	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid2 49460. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈)))
Theorem	fucoid2 49460	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid 49459. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈)))
Theorem	fuco22a 49461*	The morphism part of the functor composition bifunctor. See also fuco22 49450. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘((1st ‘𝑀)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑀)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑅)‘((1st ‘𝑀)‘𝑥)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐾)((1st ‘𝑀)‘𝑥))‘(𝐴‘𝑥)))))
Theorem	fuco23alem 49462	The naturality property (nati 17865) in category 𝐸. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ · = (comp‘𝐸)    ⇒   ⊢ (𝜑 → ((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(𝐵‘(𝐹‘𝑋))))
Theorem	fuco23a 49463	The morphism part of the functor composition bifunctor. An alternate definition of ∘F. See also fuco23 49452. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋))))    ⇒   ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋)) ∗ (𝐵‘(𝐹‘𝑋))))
Theorem	fucocolem1 49464	Lemma for fucoco 49468. 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 49465*	Lemma for fucoco 49468. 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 49466*	Lemma for fucoco 49468. 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 49467*	Lemma for fucoco 49468. 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 49468	Composition in the source category is mapped to composition in the target. See also fucoco2 49469. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ · = (comp‘𝑇)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))
Theorem	fucoco2 49469	Composition in the source category is mapped to composition in the target. See also fucoco 49468. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ · = (comp‘𝑇)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐽𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))
Theorem	fucofunc 49470	The functor composition bifunctor is a functor. See also fucofunca 49471. 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 49584), for example, (SetCat‘1o) (the trivial category, setc1oterm 49602), 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 49452. 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 49428 up to fuco23 49452, but ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) might be mapped to a different morphism in category 𝐸. See fucofulem2 49422 for some insights. 2. fuco22nat 49457, fucoid 49459, and fucoco 49468 are satisfied. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑂(𝑇 Func 𝑄)𝑃)
Theorem	fucofunca 49471	The functor composition bifunctor is a functor. See also fucofunc 49470. (Contributed by Zhi Wang, 10-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) ∈ (𝑇 Func 𝑄))
Theorem	fucolid 49472*	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 49473*	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 49474	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 49475*	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 49476	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 49477	Lemma for precofval 49478 to enable catlid 17589 or catrid 17590. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((((𝐹‘𝑋)𝐿(𝐹‘𝑋))‘(( 1 ∘ 𝐹)‘𝑋)) = (𝐼‘(𝐾‘(𝐹‘𝑋))) ∧ (𝐾‘(𝐹‘𝑋)) ∈ 𝐵))
Theorem	precofval 49478*	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 49479*	Alternate proof of precofval 49478. (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 49480*	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 49481	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 49482*	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 49483*	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 49484	Extend class notation with pre-composition functors.
class −∘F
Definition	df-prcof 49485*	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 49482). But such definition requires an explicit third category. prcoftposcurfuco 49494 and prcoftposcurfucoa 49495 prove the equivalence. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ −∘F = (𝑝 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩)
Theorem	reldmprcof 49486	The domain of −∘F is a relation. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ Rel dom −∘F
Theorem	prcofvalg 49487*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑉)    &   ⊢ (𝜑 → (1st ‘𝑃) = 𝐷)    &   ⊢ (𝜑 → (2nd ‘𝑃) = 𝐸)    ⇒   ⊢ (𝜑 → (𝑃 −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩)
Theorem	prcofvala 49488*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func 𝐹)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩)
Theorem	prcofval 49489*	Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ Rel 𝑅    &   ⊢ (𝜑 → 𝐹𝑅𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) = ⟨(𝑘 ∈ 𝐵 ↦ (𝑘 ∘func ⟨𝐹, 𝐺⟩)), (𝑘 ∈ 𝐵, 𝑙 ∈ 𝐵 ↦ (𝑎 ∈ (𝑘𝑁𝑙) ↦ (𝑎 ∘ 𝐹)))⟩)
Theorem	prcofpropd 49490	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 49491	The pre-composition functor is an ordered pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑃 −∘F 𝐹) ∈ (V × V))
Theorem	reldmprcof1 49492	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 49493	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 49494	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 49495	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 49496	The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F ⟨𝐹, 𝐺⟩) ∈ (𝑅 Func 𝑆))
Theorem	prcoffunca 49497	The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) ∈ (𝑅 Func 𝑆))
Theorem	prcoffunca2 49498	The pre-composition functor is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐾, 𝐿⟩)    ⇒   ⊢ (𝜑 → 𝐾(𝑅 Func 𝑆)𝐿)
Theorem	prcof1 49499	The object part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → (1st ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑂)    ⇒   ⊢ (𝜑 → (𝑂‘𝐾) = (𝐾 ∘func 𝐹))
Theorem	prcof2a 49500*	The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)) = 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐾𝑃𝐿) = (𝑎 ∈ (𝐾𝑁𝐿) ↦ (𝑎 ∘ (1st ‘𝐹))))