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	termoeu2 49901	Terminal objects are essentially unique; if 𝐴 is a terminal object, then so is every object that is isomorphic to 𝐴. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐴( ≃𝑐 ‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))
Theorem	initopropdlemlem 49902	Lemma for initopropdlem 49903, termopropdlem 49904, and zeroopropdlem 49905. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ 𝐹 Fn 𝑋    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑌)    &   ⊢ 𝑋 ⊆ 𝑌    &   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → (𝐹‘𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))
Theorem	initopropdlem 49903	Lemma for initopropd 49906. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → ¬ 𝐶 ∈ V)    ⇒   ⊢ (𝜑 → (InitO‘𝐶) = (InitO‘𝐷))
Theorem	termopropdlem 49904	Lemma for termopropd 49907. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → ¬ 𝐶 ∈ V)    ⇒   ⊢ (𝜑 → (TermO‘𝐶) = (TermO‘𝐷))
Theorem	zeroopropdlem 49905	Lemma for zeroopropd 49908. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → ¬ 𝐶 ∈ V)    ⇒   ⊢ (𝜑 → (ZeroO‘𝐶) = (ZeroO‘𝐷))
Theorem	initopropd 49906	Two structures with the same base, hom-sets and composition operation have the same initial objects. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    ⇒   ⊢ (𝜑 → (InitO‘𝐶) = (InitO‘𝐷))
Theorem	termopropd 49907	Two structures with the same base, hom-sets and composition operation have the same terminal objects. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    ⇒   ⊢ (𝜑 → (TermO‘𝐶) = (TermO‘𝐷))
Theorem	zeroopropd 49908	Two structures with the same base, hom-sets and composition operation have the same zero objects. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    ⇒   ⊢ (𝜑 → (ZeroO‘𝐶) = (ZeroO‘𝐷))
21.50.15.13  Product of categories
Theorem	reldmxpc 49909	The binary product of categories is a proper operator, so it can be used with ovprc1 7450, elbasov 17276, strov2rcl 17277, and so on. See reldmxpcALT 49910 for an alternate proof with less "essential steps" but more "bytes". (Proposed by SN, 15-Oct-2025.) (Contributed by Zhi Wang, 15-Oct-2025.)
⊢ Rel dom ×c
Theorem	reldmxpcALT 49910	Alternate proof of reldmxpc 49909. (Contributed by Zhi Wang, 15-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Rel dom ×c
Theorem	elxpcbasex1 49911	A non-empty base set of the product category indicates the existence of the first factor of the product category. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof shortened by SN, 15-Oct-2025.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ V)
Theorem	elxpcbasex1ALT 49912	Alternate proof of elxpcbasex1 49911. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ V)
Theorem	elxpcbasex2 49913	A non-empty base set of the product category indicates the existence of the second factor of the product category. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof shortened by SN, 15-Oct-2025.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 ∈ V)
Theorem	elxpcbasex2ALT 49914	Alternate proof of elxpcbasex2 49913. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 ∈ V)
Theorem	xpcfucbas 49915	The base set of the product of two categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸))    ⇒   ⊢ ((𝐵 Func 𝐶) × (𝐷 Func 𝐸)) = (Base‘𝑇)
Theorem	xpcfuchomfval 49916*	Set of morphisms of the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸))    &   ⊢ 𝐴 = (Base‘𝑇)    &   ⊢ 𝐾 = (Hom ‘𝑇)    ⇒   ⊢ 𝐾 = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐴 ↦ (((1st ‘𝑢)(𝐵 Nat 𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(𝐷 Nat 𝐸)(2nd ‘𝑣))))
Theorem	xpcfuchom 49917	Set of morphisms of the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸))    &   ⊢ 𝐴 = (Base‘𝑇)    &   ⊢ 𝐾 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = (((1st ‘𝑋)(𝐵 Nat 𝐶)(1st ‘𝑌)) × ((2nd ‘𝑋)(𝐷 Nat 𝐸)(2nd ‘𝑌))))
Theorem	xpcfuchom2 49918	Value of the set of morphisms in the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸))    &   ⊢ (𝜑 → 𝑀 ∈ (𝐵 Func 𝐶))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 Func 𝐶))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐾 = (Hom ‘𝑇)    ⇒   ⊢ (𝜑 → (⟨𝑀, 𝑁⟩𝐾⟨𝑃, 𝑄⟩) = ((𝑀(𝐵 Nat 𝐶)𝑃) × (𝑁(𝐷 Nat 𝐸)𝑄)))
Theorem	xpcfucco2 49919	Value of composition in the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸))    &   ⊢ 𝑂 = (comp‘𝑇)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆))    ⇒   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) = ⟨(𝐾(⟨𝑀, 𝑃⟩(comp‘(𝐵 FuncCat 𝐶))𝑅)𝐹), (𝐿(⟨𝑁, 𝑄⟩(comp‘(𝐷 FuncCat 𝐸))𝑆)𝐺)⟩)
Theorem	xpcfuccocl 49920	The composition of two natural transformations is a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸))    &   ⊢ 𝑂 = (comp‘𝑇)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆))    ⇒   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) ∈ ((𝑀(𝐵 Nat 𝐶)𝑅) × (𝑁(𝐷 Nat 𝐸)𝑆)))
Theorem	xpcfucco3 49921*	Value of composition in the binary product of categories of functors; expressed explicitly. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸))    &   ⊢ 𝑂 = (comp‘𝑇)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆))    &   ⊢ 𝑋 = (Base‘𝐵)    &   ⊢ 𝑌 = (Base‘𝐷)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐸)    ⇒   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) = ⟨(𝑥 ∈ 𝑋 ↦ ((𝐾‘𝑥)(⟨((1st ‘𝑀)‘𝑥), ((1st ‘𝑃)‘𝑥)⟩ · ((1st ‘𝑅)‘𝑥))(𝐹‘𝑥))), (𝑦 ∈ 𝑌 ↦ ((𝐿‘𝑦)(⟨((1st ‘𝑁)‘𝑦), ((1st ‘𝑄)‘𝑦)⟩ ∙ ((1st ‘𝑆)‘𝑦))(𝐺‘𝑦)))⟩)
21.50.15.14  Swap functors
Syntax	cswapf 49922	Extend class notation with the class of swap functors.
class swapF
Definition	df-swapf 49923*	Define the swap functor from (𝐶 ×c 𝐷) to (𝐷 ×c 𝐶) by swapping all objects (swapf1 49935) and morphisms (swapf2 49937) . Such functor is called a "swap functor" in https://arxiv.org/pdf/2302.07810 49937 or a "twist functor" in https://arxiv.org/pdf/2508.01886 49937, the latter of which finds its counterpart as "twisting map" in https://arxiv.org/pdf/2411.04102 49937 for tensor product of algebras. The "swap functor" or "twisting map" is often denoted as a small tau 𝜏 in literature. However, the term "twist functor" is defined differently in https://arxiv.org/pdf/1208.4046 49937 and thus not adopted here. tpos I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 49924 for an alternate definition. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)
Theorem	dfswapf2 49924*	Alternate definition of swapF (df-swapf 49923). (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(tpos I ↾ 𝑏), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (tpos I ↾ (𝑢ℎ𝑣)))⟩)
Theorem	swapfval 49925*	Value of the swap functor. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    ⇒   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨(𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))⟩)
Theorem	swapfelvv 49926	A swap functor is an ordered pair. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (V × V))
Theorem	swapf2fvala 49927*	The morphism part of the swap functor. See also swapf2fval 49928. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    ⇒   ⊢ (𝜑 → (2nd ‘(𝐶 swapF 𝐷)) = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓})))
Theorem	swapf2fval 49928*	The morphism part of the swap functor. See also swapf2fvala 49927. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑃 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓})))
Theorem	swapf1vala 49929*	The object part of the swap functor. See also swapf1val 49930. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → (1st ‘(𝐶 swapF 𝐷)) = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}))
Theorem	swapf1val 49930*	The object part of the swap functor. See also swapf1vala 49929. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑂 = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}))
Theorem	swapf2fn 49931	The morphism part of the swap functor is a function on the Cartesian square of the base set. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑃 Fn (𝐵 × 𝐵))
Theorem	swapf1a 49932	The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑂‘𝑋) = ⟨(2nd ‘𝑋), (1st ‘𝑋)⟩)
Theorem	swapf2vala 49933*	The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    ⇒   ⊢ (𝜑 → (𝑋𝑃𝑌) = (𝑓 ∈ (𝑋𝐻𝑌) ↦ ∪ ◡{𝑓}))
Theorem	swapf2a 49934	The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑌)‘𝐹) = ⟨(2nd ‘𝐹), (1st ‘𝐹)⟩)
Theorem	swapf1 49935	The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷))    ⇒   ⊢ (𝜑 → (𝑋𝑂𝑌) = ⟨𝑌, 𝑋⟩)
Theorem	swapf2val 49936*	The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷))    &   ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐷))    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑃⟨𝑍, 𝑊⟩) = (𝑓 ∈ (⟨𝑋, 𝑌⟩𝐻⟨𝑍, 𝑊⟩) ↦ ∪ ◡{𝑓}))
Theorem	swapf2 49937	The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷))    &   ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐷))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑍))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌(Hom ‘𝐷)𝑊))    ⇒   ⊢ (𝜑 → (𝐹(⟨𝑋, 𝑌⟩𝑃⟨𝑍, 𝑊⟩)𝐺) = ⟨𝐺, 𝐹⟩)
Theorem	swapf1f1o 49938	The object part of the swap functor is a bijection between base sets. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (Base‘𝑇)    ⇒   ⊢ (𝜑 → 𝑂:𝐵–1-1-onto→𝐴)
Theorem	swapf2f1o 49939	The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ 𝐻 = (Hom ‘𝑆)    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷))    &   ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐷))    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑃⟨𝑍, 𝑊⟩):(⟨𝑋, 𝑌⟩𝐻⟨𝑍, 𝑊⟩)–1-1-onto→(⟨𝑌, 𝑋⟩𝐽⟨𝑊, 𝑍⟩))
Theorem	swapf2f1oa 49940	The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ 𝐻 = (Hom ‘𝑆)    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑃𝑌):(𝑋𝐻𝑌)–1-1-onto→((𝑂‘𝑋)𝐽(𝑂‘𝑌)))
Theorem	swapf2f1oaALT 49941	Alternate proof of swapf2f1oa 49940. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ 𝐻 = (Hom ‘𝑆)    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑃𝑌):(𝑋𝐻𝑌)–1-1-onto→((𝑂‘𝑋)𝐽(𝑂‘𝑌)))
Theorem	swapfid 49942	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfida 49943. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷))    &   ⊢ 1 = (Id‘𝑆)    &   ⊢ 𝐼 = (Id‘𝑇)    ⇒   ⊢ (𝜑 → ((⟨𝑋, 𝑌⟩𝑃⟨𝑋, 𝑌⟩)‘( 1 ‘⟨𝑋, 𝑌⟩)) = (𝐼‘(𝑂‘⟨𝑋, 𝑌⟩)))
Theorem	swapfida 49943	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfid 49942. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 1 = (Id‘𝑆)    &   ⊢ 𝐼 = (Id‘𝑇)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝑂‘𝑋)))
Theorem	swapfcoa 49944	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 49945	The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑂(𝑆 Func 𝑇)𝑃)
Theorem	swapfffth 49946	The swap functor is a fully faithful functor. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑂((𝑆 Full 𝑇) ∩ (𝑆 Faith 𝑇))𝑃)
Theorem	swapffunca 49947	The swap functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (𝑆 Func 𝑇))
Theorem	swapfiso 49948	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 49949	The product category is categorically isomorphic to the swapped product category. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑆( ≃𝑐 ‘𝐸)𝑇)
21.50.15.15  Functor evaluation
Theorem	oppc1stflem 49950*	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 49951	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 49952	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 49953	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 49954	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 49955	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.50.15.16  Transposed curry functors
Theorem	cofuswapfcl 49956	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 49957	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 49958	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 49959	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 49960	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 49961	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 49962*	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 49963*	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 49964	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 49965	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 49966	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.50.15.17  Constant functors
Theorem	diag1 49967*	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 49968*	The constant functor of 𝑋. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝐵 × {𝑋}), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ ((𝑦𝐽𝑧) × {( 1 ‘𝑋)}))⟩)
Theorem	diag1f1lem 49969	The object part of the diagonal functor is 1-1 if 𝐵 is non-empty. Note that (𝜑 → (𝑀 = 𝑁 ↔ 𝑋 = 𝑌)) also holds because of diag1f1 49970 and f1fveq 7261. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ 𝑀 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝑁 = ((1st ‘𝐿)‘𝑌)    ⇒   ⊢ (𝜑 → (𝑀 = 𝑁 → 𝑋 = 𝑌))
Theorem	diag1f1 49970	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 49971	Lemma for diag2f1 49972. The converse is trivial (fveq2 6882). (Contributed by Zhi Wang, 21-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = ((𝑋(2nd ‘𝐿)𝑌)‘𝐺) → 𝐹 = 𝐺))
Theorem	diag2f1 49972	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.50.15.18  Functor composition bifunctors
Theorem	fucofulem1 49973	Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))    &   ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜏)) → 𝜂)    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜂) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜂) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜂))
Theorem	fucofulem2 49974*	Lemma for proving functor theorems. Maybe consider eufnfv 7228 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 49975	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩ ∈ (𝑆 × 𝑅) ↔ (𝐾𝑆𝐿 ∧ 𝐹𝑅𝐺))
Theorem	fuco2eld 49976	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝐾𝑆𝐿)    &   ⊢ (𝜑 → 𝐹𝑅𝐺)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑊)
Theorem	fuco2eld2 49977	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝑈 = ⟨⟨(1st ‘(1st ‘𝑈)), (2nd ‘(1st ‘𝑈))⟩, ⟨(1st ‘(2nd ‘𝑈)), (2nd ‘(2nd ‘𝑈))⟩⟩)
Theorem	fuco2eld3 49978	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → ((1st ‘(1st ‘𝑈))𝑆(2nd ‘(1st ‘𝑈)) ∧ (1st ‘(2nd ‘𝑈))𝑅(2nd ‘(2nd ‘𝑈))))
Syntax	cfuco 49979	Extend class notation with functor composition bifunctors.
class ∘F
Definition	df-fuco 49980*	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 50022). The object part maps two functors to their composition (fuco11 49989 and fuco11b 50000). The morphism part defines the "composition" of two natural transformations (fuco22 50002) into another natural transformation (fuco22nat 50009) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 50015). Note that such "composition" is different from fucco 18022 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 49981*	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 49982*	Value of the function giving the functor composition bifunctor. Hypotheses fucofval.c and fucofval.d are not redundant (fucofvalne 49988). (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 49983	A functor composition bifunctor is an ordered pair. Enables 1st2ndb 8026. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    ⇒   ⊢ (𝜑 → ⚬ ∈ (V × V))
Theorem	fuco1 49984	The object part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑂 = ( ∘func ↾ 𝑊))
Theorem	fucof1 49985	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 49986*	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 49987	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 49988*	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 49989	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 49990	The object part of the functor composition bifunctor maps into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) ∈ (𝐶 Func 𝐸))
Theorem	fuco11a 49991*	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 49992*	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 49993	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 49994	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 49995	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 49996	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 49997	The identity morphism of the mapped object. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑂‘𝑈)) = ( 1 ∘ (𝐾 ∘ 𝐹)))
Theorem	fuco11idx 49998	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 49999*	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 50000	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 𝐹))