P. 493 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49201-49300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oppcup3lem 49201*	Lemma for oppcup3 49204. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ ((𝐹‘𝑦)𝐽𝑍)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑛 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩𝑂𝑍)((𝑦𝐺𝑋)‘𝑘)))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ((𝐹‘𝑌)𝐽𝑍))    ⇒   ⊢ (𝜑 → ∃!𝑙 ∈ (𝑌𝐻𝑋)𝑁 = (𝑀(⟨(𝐹‘𝑌), (𝐹‘𝑋)⟩𝑂𝑍)((𝑌𝐺𝑋)‘𝑙)))
Theorem	oppcup 49202*	The universal pair ⟨𝑋, 𝑀⟩ from a functor to an object is universal from an object to a functor in the opposite category. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ ∙ = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ((𝐹‘𝑋)𝐽𝑊))    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝑃 = (oppCat‘𝐸)    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, tpos 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ ((𝐹‘𝑦)𝐽𝑊)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑔 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩ ∙ 𝑊)((𝑦𝐺𝑋)‘𝑘))))
Theorem	oppcup2 49203*	The universal property for the universal pair ⟨𝑋, 𝑀⟩ from a functor to an object, expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ ∙ = (comp‘𝐸)    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋(⟨𝐹, tpos 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀)    ⇒   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ ((𝐹‘𝑦)𝐽𝑊)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑔 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩ ∙ 𝑊)((𝑦𝐺𝑋)‘𝑘)))
Theorem	oppcup3 49204*	The universal property for the universal pair ⟨𝑋, 𝑀⟩ from a functor to an object, expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ ∙ = (comp‘𝐸)    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ (𝜑 → 𝑋(⟨𝐹, 𝑇⟩(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ (𝜑 → tpos 𝑇 = 𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ((𝐹‘𝑌)𝐽𝑊))    ⇒   ⊢ (𝜑 → ∃!𝑘 ∈ (𝑌𝐻𝑋)𝑁 = (𝑀(⟨(𝐹‘𝑌), (𝐹‘𝑋)⟩ ∙ 𝑊)((𝑌𝐺𝑋)‘𝑘)))
Theorem	uptrlem1 49205*	Lemma for uptr 49208. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ ⚬ = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷))    &   ⊢ (𝜑 → (𝑀‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝐹‘𝑍)))    &   ⊢ (𝜑 → ((𝑋𝑁(𝐹‘𝑍))‘𝐴) = 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑀((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑁)    &   ⊢ (𝜑 → (⟨𝑀, 𝑁⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩)    ⇒   ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽(𝐾‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ ∀𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴)))
Theorem	uptrlem2 49206*	Lemma for uptr 49208. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ ⚬ = (comp‘𝐸)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼((1st ‘𝐹)‘𝑍)))    &   ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    ⇒   ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽((1st ‘𝐺)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍(2nd ‘𝐺)𝑊)‘𝑘)(⟨𝑌, ((1st ‘𝐺)‘𝑍)⟩ ⚬ ((1st ‘𝐺)‘𝑊))𝑁) ↔ ∀𝑔 ∈ (𝑋𝐼((1st ‘𝐹)‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍(2nd ‘𝐹)𝑊)‘𝑘)(⟨𝑋, ((1st ‘𝐹)‘𝑍)⟩ ∙ ((1st ‘𝐹)‘𝑊))𝑀)))
Theorem	uptrlem3 49207	Lemma for uptr 49208. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ (𝜑 → (𝑅‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆)    &   ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍)))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁))
Theorem	uptr 49208	Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ (𝜑 → (𝑅‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆)    &   ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍)))    ⇒   ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁))
Theorem	uptri 49209	Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ (𝜑 → (𝑅‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆)    &   ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁)    &   ⊢ (𝜑 → 𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀)    ⇒   ⊢ (𝜑 → 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)
Theorem	uptra 49210	Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽((1st ‘𝐹)‘𝑍)))    ⇒   ⊢ (𝜑 → (𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁))
Theorem	uptrar 49211	Universal property and fully faithful functor. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → (◡(𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑁) = 𝑀)    &   ⊢ (𝜑 → 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁)    ⇒   ⊢ (𝜑 → 𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀)
Theorem	uptrai 49212	Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    &   ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁)    &   ⊢ (𝜑 → 𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀)    ⇒   ⊢ (𝜑 → 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁)
Theorem	uobffth 49213	A fully faithful functor generates equal sets of universal objects. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    &   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))    ⇒   ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌))
Theorem	uobeqw 49214	If a full functor (in fact, a full embedding) is a section of a fully faithful functor (surjective on objects), then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    &   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Full 𝐸))    &   ⊢ (𝜑 → (𝐿 ∘func 𝐾) = 𝐼)    &   ⊢ (𝜑 → 𝐿 ∈ ((𝐸 Full 𝐷) ∩ (𝐸 Faith 𝐷)))    ⇒   ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌))
Theorem	uobeq 49215	If a full functor (in fact, a full embedding) is a section of a functor (surjective on objects), then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺)    &   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌)    &   ⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Full 𝐸))    &   ⊢ (𝜑 → (𝐿 ∘func 𝐾) = 𝐼)    &   ⊢ (𝜑 → 𝐿 ∈ (𝐸 Func 𝐷))    ⇒   ⊢ (𝜑 → dom (𝐹(𝐶 UP 𝐷)𝑋) = dom (𝐺(𝐶 UP 𝐸)𝑌))
Theorem	uptr2 49216	Universal property and fully faithful functor surjective on objects. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 = (𝑅‘𝑋))    &   ⊢ (𝜑 → 𝑅:𝐴–onto→𝐵)    &   ⊢ (𝜑 → 𝑅((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝑆)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝑅, 𝑆⟩) = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐶 UP 𝐸)𝑍)𝑀 ↔ 𝑌(⟨𝐾, 𝐿⟩(𝐷 UP 𝐸)𝑍)𝑀))
Theorem	uptr2a 49217	Universal property and fully faithful functor surjective on objects. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 = ((1st ‘𝐾)‘𝑋))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐾) = 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐾 ∈ ((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷)))    &   ⊢ (𝜑 → (1st ‘𝐾):𝐴–onto→𝐵)    ⇒   ⊢ (𝜑 → (𝑋(𝐹(𝐶 UP 𝐸)𝑍)𝑀 ↔ 𝑌(𝐺(𝐷 UP 𝐸)𝑍)𝑀))
21.49.15.11  Natural transformations and the functor category
Theorem	isnatd 49218*	Property of being a natural transformation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿)    &   ⊢ (𝜑 → 𝐴 Fn 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐴‘𝑥) ∈ ((𝐹‘𝑥)𝐽(𝐾‘𝑥)))    &   ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ℎ ∈ (𝑥𝐻𝑦)) → ((𝐴‘𝑦)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(⟨(𝐹‘𝑥), (𝐾‘𝑥)⟩ · (𝐾‘𝑦))(𝐴‘𝑥)))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))
Theorem	natrcl2 49219	Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)
Theorem	natrcl3 49220	Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    ⇒   ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿)
Theorem	catbas 49221	The base of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩}    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ 𝐵 = (Base‘𝐶)
Theorem	cathomfval 49222	The hom-sets of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩}    &   ⊢ 𝐻 ∈ V    ⇒   ⊢ 𝐻 = (Hom ‘𝐶)
Theorem	catcofval 49223	Composition of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩}    &   ⊢ · ∈ V    ⇒   ⊢ · = (comp‘𝐶)
Theorem	natoppf 49224	A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝑀 = (𝑂 Nat 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐾, tpos 𝐿⟩𝑀⟨𝐹, tpos 𝐺⟩))
Theorem	natoppf2 49225	A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝑀 = (𝑂 Nat 𝑃)    &   ⊢ (𝜑 → 𝐾 = ( oppFunc ‘𝐹))    &   ⊢ (𝜑 → 𝐿 = ( oppFunc ‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐿𝑀𝐾))
Theorem	natoppfb 49226	A natural transformation is natural between opposite functors, and vice versa. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝑀 = (𝑂 Nat 𝑃)    &   ⊢ (𝜑 → 𝐾 = ( oppFunc ‘𝐹))    &   ⊢ (𝜑 → 𝐿 = ( oppFunc ‘𝐺))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹𝑁𝐺) = (𝐿𝑀𝐾))
21.49.15.12  Initial, terminal and zero objects of a category
Theorem	initoo2 49227	An initial object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ 𝐵)
Theorem	termoo2 49228	A terminal object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ 𝐵)
Theorem	zeroo2 49229	A zero object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑂 ∈ (ZeroO‘𝐶) → 𝑂 ∈ 𝐵)
Theorem	oppcinito 49230	Initial objects are terminal in the opposite category. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ (TermO‘(oppCat‘𝐶)))
Theorem	oppctermo 49231	Terminal objects are initial in the opposite category. Comments before Definition 7.4 in [Adamek] p. 102. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝐼 ∈ (TermO‘𝐶) ↔ 𝐼 ∈ (InitO‘(oppCat‘𝐶)))
Theorem	oppczeroo 49232	Zero objects are zero in the opposite category. Remark 7.8 of [Adamek] p. 103. (Contributed by Zhi Wang, 27-Oct-2025.)
⊢ (𝐼 ∈ (ZeroO‘𝐶) ↔ 𝐼 ∈ (ZeroO‘(oppCat‘𝐶)))
Theorem	termoeu2 49233	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 49234	Lemma for initopropdlem 49235, termopropdlem 49236, and zeroopropdlem 49237. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ 𝐹 Fn 𝑋    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑌)    &   ⊢ 𝑋 ⊆ 𝑌    &   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → (𝐹‘𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))
Theorem	initopropdlem 49235	Lemma for initopropd 49238. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → ¬ 𝐶 ∈ V)    ⇒   ⊢ (𝜑 → (InitO‘𝐶) = (InitO‘𝐷))
Theorem	termopropdlem 49236	Lemma for termopropd 49239. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → ¬ 𝐶 ∈ V)    ⇒   ⊢ (𝜑 → (TermO‘𝐶) = (TermO‘𝐷))
Theorem	zeroopropdlem 49237	Lemma for zeroopropd 49240. (Contributed by Zhi Wang, 26-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → ¬ 𝐶 ∈ V)    ⇒   ⊢ (𝜑 → (ZeroO‘𝐶) = (ZeroO‘𝐷))
Theorem	initopropd 49238	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 49239	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 49240	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.49.15.13  Product of categories
Theorem	reldmxpc 49241	The binary product of categories is a proper operator, so it can be used with ovprc1 7388, elbasov 17127, strov2rcl 17128, and so on. See reldmxpcALT 49242 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 49242	Alternate proof of reldmxpc 49241. (Contributed by Zhi Wang, 15-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Rel dom ×c
Theorem	elxpcbasex1 49243	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 49244	Alternate proof of elxpcbasex1 49243. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ V)
Theorem	elxpcbasex2 49245	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 49246	Alternate proof of elxpcbasex2 49245. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 ∈ V)
Theorem	xpcfucbas 49247	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 49248*	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 49249	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 49250	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 49251	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 49252	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 49253*	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.49.15.14  Swap functors
Syntax	cswapf 49254	Extend class notation with the class of swap functors.
class swapF
Definition	df-swapf 49255*	Define the swap functor from (𝐶 ×c 𝐷) to (𝐷 ×c 𝐶) by swapping all objects (swapf1 49267) and morphisms (swapf2 49269) . Such functor is called a "swap functor" in https://arxiv.org/pdf/2302.07810 49269 or a "twist functor" in https://arxiv.org/pdf/2508.01886 49269, the latter of which finds its counterpart as "twisting map" in https://arxiv.org/pdf/2411.04102 49269 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 49269 and thus not adopted here. tpos I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 49256 for an alternate definition. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)
Theorem	dfswapf2 49256*	Alternate definition of swapF (df-swapf 49255). (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(tpos I ↾ 𝑏), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (tpos I ↾ (𝑢ℎ𝑣)))⟩)
Theorem	swapfval 49257*	Value of the swap functor. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    ⇒   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨(𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))⟩)
Theorem	swapfelvv 49258	A swap functor is an ordered pair. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (V × V))
Theorem	swapf2fvala 49259*	The morphism part of the swap functor. See also swapf2fval 49260. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    ⇒   ⊢ (𝜑 → (2nd ‘(𝐶 swapF 𝐷)) = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓})))
Theorem	swapf2fval 49260*	The morphism part of the swap functor. See also swapf2fvala 49259. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑃 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓})))
Theorem	swapf1vala 49261*	The object part of the swap functor. See also swapf1val 49262. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → (1st ‘(𝐶 swapF 𝐷)) = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}))
Theorem	swapf1val 49262*	The object part of the swap functor. See also swapf1vala 49261. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑂 = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}))
Theorem	swapf2fn 49263	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 49264	The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑂‘𝑋) = ⟨(2nd ‘𝑋), (1st ‘𝑋)⟩)
Theorem	swapf2vala 49265*	The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆))    ⇒   ⊢ (𝜑 → (𝑋𝑃𝑌) = (𝑓 ∈ (𝑋𝐻𝑌) ↦ ∪ ◡{𝑓}))
Theorem	swapf2a 49266	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 49267	The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷))    ⇒   ⊢ (𝜑 → (𝑋𝑂𝑌) = ⟨𝑌, 𝑋⟩)
Theorem	swapf2val 49268*	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 49269	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 49270	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 49271	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 49272	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 49273	Alternate proof of swapf2f1oa 49272. (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 49274	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfida 49275. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷))    &   ⊢ 1 = (Id‘𝑆)    &   ⊢ 𝐼 = (Id‘𝑇)    ⇒   ⊢ (𝜑 → ((⟨𝑋, 𝑌⟩𝑃⟨𝑋, 𝑌⟩)‘( 1 ‘⟨𝑋, 𝑌⟩)) = (𝐼‘(𝑂‘⟨𝑋, 𝑌⟩)))
Theorem	swapfida 49275	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfid 49274. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 1 = (Id‘𝑆)    &   ⊢ 𝐼 = (Id‘𝑇)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝑂‘𝑋)))
Theorem	swapfcoa 49276	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 49277	The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑂(𝑆 Func 𝑇)𝑃)
Theorem	swapfffth 49278	The swap functor is a fully faithful functor. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → 𝑂((𝑆 Full 𝑇) ∩ (𝑆 Faith 𝑇))𝑃)
Theorem	swapffunca 49279	The swap functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (𝑆 Func 𝑇))
Theorem	swapfiso 49280	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 49281	The product category is categorically isomorphic to the swapped product category. (Contributed by Zhi Wang, 8-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑆 = (𝐶 ×c 𝐷)    &   ⊢ 𝑇 = (𝐷 ×c 𝐶)    &   ⊢ 𝐸 = (CatCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑆( ≃𝑐 ‘𝐸)𝑇)
21.49.15.15  Functor evaluation
Theorem	oppc1stflem 49282*	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 49283	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 49284	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 49285	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 49286	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 49287	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 49288	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 49289	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 49290	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 49291	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 49292	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 49293	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 49294*	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 49295*	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 49296	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 49297	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 49298	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 49299*	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 49300*	The constant functor of 𝑋. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝐵 × {𝑋}), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ ((𝑦𝐽𝑧) × {( 1 ‘𝑋)}))⟩)