HomeTheorem List (p. 494 of 500)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 494 of 500) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30898) |
Hilbert Space Explorer
(30899-32421) |
Users' Mathboxes
(32422-49905) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | oppcuprcl5 49301 | Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝑃 = (oppCat‘𝐸) & ⊢ 𝐽 = (Hom ‘𝐸) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐹‘𝑋)𝐽𝑊)) | ||
| Theorem | oppcuprcl2 49302 | Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝑃 = (oppCat‘𝐸) & ⊢ 𝑂 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → tpos 𝐺 = 𝐻) ⇒ ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐻) | ||
| Theorem | uprcl2a 49303 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(𝐺(𝑂 UP 𝑃)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑃)) | ||
| Theorem | oppfuprcl 49304 | Reverse closure for the class of universal property for opposite functors. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(𝐺(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝐺 = ( oppFunc ‘𝐹) & ⊢ 𝑂 = (oppCat‘𝐷) & ⊢ 𝑃 = (oppCat‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) | ||
| Theorem | oppfuprcl2 49305 | Reverse closure for the class of universal property for opposite functors. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(𝐺(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝐺 = ( oppFunc ‘𝐹) & ⊢ 𝑂 = (oppCat‘𝐷) & ⊢ 𝑃 = (oppCat‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩) ⇒ ⊢ (𝜑 → 𝐴(𝐷 Func 𝐸)𝐵) | ||
| Theorem | oppcup3lem 49306* | Lemma for oppcup3 49309. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ ((𝐹‘𝑦)𝐽𝑍)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑛 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩𝑂𝑍)((𝑦𝐺𝑋)‘𝑘))) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ((𝐹‘𝑌)𝐽𝑍)) ⇒ ⊢ (𝜑 → ∃!𝑙 ∈ (𝑌𝐻𝑋)𝑁 = (𝑀(⟨(𝐹‘𝑌), (𝐹‘𝑋)⟩𝑂𝑍)((𝑌𝐺𝑋)‘𝑙))) | ||
| Theorem | oppcup 49307* | 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 49308* | 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 49309* | 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 49310* | Lemma for uptr 49313. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ ∙ = (comp‘𝐷) & ⊢ ⚬ = (comp‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷)) & ⊢ (𝜑 → (𝑀‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝐹‘𝑍))) & ⊢ (𝜑 → ((𝑋𝑁(𝐹‘𝑍))‘𝐴) = 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝑀((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑁) & ⊢ (𝜑 → (⟨𝑀, 𝑁⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) ⇒ ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽(𝐾‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ ∀𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴))) | ||
| Theorem | uptrlem2 49311* | Lemma for uptr 49313. (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 49312 | Lemma for uptr 49313. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptr 49313 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍))) ⇒ ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptri 49314 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uptra 49315 | 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 49316 | 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 49317 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uobffth 49318 | 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 49319 | 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 49320 | 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 49321 | 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 49322 | 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 𝐸)𝑍)𝑀)) | ||
| Theorem | isnatd 49323* | 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 49324 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | ||
| Theorem | natrcl3 49325 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) | ||
| Theorem | catbas 49326 | The base of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ 𝐵 ∈ V ⇒ ⊢ 𝐵 = (Base‘𝐶) | ||
| Theorem | cathomfval 49327 | The hom-sets of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ 𝐻 ∈ V ⇒ ⊢ 𝐻 = (Hom ‘𝐶) | ||
| Theorem | catcofval 49328 | Composition of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ · ∈ V ⇒ ⊢ · = (comp‘𝐶) | ||
| Theorem | natoppf 49329 | A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝑀 = (𝑂 Nat 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (⟨𝐾, tpos 𝐿⟩𝑀⟨𝐹, tpos 𝐺⟩)) | ||
| Theorem | natoppf2 49330 | A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝑀 = (𝑂 Nat 𝑃) & ⊢ (𝜑 → 𝐾 = ( oppFunc ‘𝐹)) & ⊢ (𝜑 → 𝐿 = ( oppFunc ‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐿𝑀𝐾)) | ||
| Theorem | natoppfb 49331 | A natural transformation is natural between opposite functors, and vice versa. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝑀 = (𝑂 Nat 𝑃) & ⊢ (𝜑 → 𝐾 = ( oppFunc ‘𝐹)) & ⊢ (𝜑 → 𝐿 = ( oppFunc ‘𝐺)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹𝑁𝐺) = (𝐿𝑀𝐾)) | ||
| Theorem | initoo2 49332 | An initial object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | termoo2 49333 | A terminal object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | zeroo2 49334 | A zero object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑂 ∈ (ZeroO‘𝐶) → 𝑂 ∈ 𝐵) | ||
| Theorem | oppcinito 49335 | Initial objects are terminal in the opposite category. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ (TermO‘(oppCat‘𝐶))) | ||
| Theorem | oppctermo 49336 | 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 49337 | 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 49338 | 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 49339 | Lemma for initopropdlem 49340, termopropdlem 49341, and zeroopropdlem 49342. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝐹 Fn 𝑋 & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑌) & ⊢ 𝑋 ⊆ 𝑌 & ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → (𝐹‘𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵)) | ||
| Theorem | initopropdlem 49340 | Lemma for initopropd 49343. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (InitO‘𝐶) = (InitO‘𝐷)) | ||
| Theorem | termopropdlem 49341 | Lemma for termopropd 49344. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (TermO‘𝐶) = (TermO‘𝐷)) | ||
| Theorem | zeroopropdlem 49342 | Lemma for zeroopropd 49345. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → ¬ 𝐶 ∈ V) ⇒ ⊢ (𝜑 → (ZeroO‘𝐶) = (ZeroO‘𝐷)) | ||
| Theorem | initopropd 49343 | 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 49344 | 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 49345 | 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‘𝐷)) | ||
| Theorem | reldmxpc 49346 | The binary product of categories is a proper operator, so it can be used with ovprc1 7385, elbasov 17127, strov2rcl 17128, and so on. See reldmxpcALT 49347 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 49347 | Alternate proof of reldmxpc 49346. (Contributed by Zhi Wang, 15-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Rel dom ×c | ||
| Theorem | elxpcbasex1 49348 | 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 49349 | Alternate proof of elxpcbasex1 49348. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ V) | ||
| Theorem | elxpcbasex2 49350 | 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 49351 | Alternate proof of elxpcbasex2 49350. (Contributed by Zhi Wang, 8-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐷 ∈ V) | ||
| Theorem | xpcfucbas 49352 | 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 49353* | 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 49354 | 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 49355 | 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 49356 | 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 49357 | 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 49358* | 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 ‘𝑆)‘𝑦))(𝐺‘𝑦)))⟩) | ||
| Syntax | cswapf 49359 | Extend class notation with the class of swap functors. |
| class swapF | ||
| Definition | df-swapf 49360* |
Define the swap functor from (𝐶 ×c 𝐷) to (𝐷
×c 𝐶) by
swapping all objects (swapf1 49372) and morphisms (swapf2 49374) .
Such functor is called a "swap functor" in https://arxiv.org/pdf/2302.07810 49374 or a "twist functor" in https://arxiv.org/pdf/2508.01886 49374, the latter of which finds its counterpart as "twisting map" in https://arxiv.org/pdf/2411.04102 49374 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 49374 and thus not adopted here. tpos I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 49361 for an alternate definition. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩) | ||
| Theorem | dfswapf2 49361* | Alternate definition of swapF (df-swapf 49360). (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(tpos I ↾ 𝑏), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (tpos I ↾ (𝑢ℎ𝑣)))⟩) | ||
| Theorem | swapfval 49362* | Value of the swap functor. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨(𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))⟩) | ||
| Theorem | swapfelvv 49363 | A swap functor is an ordered pair. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (V × V)) | ||
| Theorem | swapf2fvala 49364* | The morphism part of the swap functor. See also swapf2fval 49365. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (2nd ‘(𝐶 swapF 𝐷)) = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))) | ||
| Theorem | swapf2fval 49365* | The morphism part of the swap functor. See also swapf2fvala 49364. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑃 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑓 ∈ (𝑢𝐻𝑣) ↦ ∪ ◡{𝑓}))) | ||
| Theorem | swapf1vala 49366* | The object part of the swap functor. See also swapf1val 49367. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝜑 → (1st ‘(𝐶 swapF 𝐷)) = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥})) | ||
| Theorem | swapf1val 49367* | The object part of the swap functor. See also swapf1vala 49366. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂 = (𝑥 ∈ 𝐵 ↦ ∪ ◡{𝑥})) | ||
| Theorem | swapf2fn 49368 | 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 49369 | The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑂‘𝑋) = ⟨(2nd ‘𝑋), (1st ‘𝑋)⟩) | ||
| Theorem | swapf2vala 49370* | The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝑆)) ⇒ ⊢ (𝜑 → (𝑋𝑃𝑌) = (𝑓 ∈ (𝑋𝐻𝑌) ↦ ∪ ◡{𝑓})) | ||
| Theorem | swapf2a 49371 | 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 49372 | The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) ⇒ ⊢ (𝜑 → (𝑋𝑂𝑌) = ⟨𝑌, 𝑋⟩) | ||
| Theorem | swapf2val 49373* | 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 49374 | 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 49375 | 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 49376 | 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 49377 | 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 49378 | Alternate proof of swapf2f1oa 49377. (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 49379 | Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfida 49380. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐷)) & ⊢ 1 = (Id‘𝑆) & ⊢ 𝐼 = (Id‘𝑇) ⇒ ⊢ (𝜑 → ((⟨𝑋, 𝑌⟩𝑃⟨𝑋, 𝑌⟩)‘( 1 ‘⟨𝑋, 𝑌⟩)) = (𝐼‘(𝑂‘⟨𝑋, 𝑌⟩))) | ||
| Theorem | swapfida 49380 | Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfid 49379. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 1 = (Id‘𝑆) & ⊢ 𝐼 = (Id‘𝑇) ⇒ ⊢ (𝜑 → ((𝑋𝑃𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝑂‘𝑋))) | ||
| Theorem | swapfcoa 49381 | 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 49382 | The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂(𝑆 Func 𝑇)𝑃) | ||
| Theorem | swapfffth 49383 | The swap functor is a fully faithful functor. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ (𝜑 → (𝐶 swapF 𝐷) = ⟨𝑂, 𝑃⟩) ⇒ ⊢ (𝜑 → 𝑂((𝑆 Full 𝑇) ∩ (𝑆 Faith 𝑇))𝑃) | ||
| Theorem | swapffunca 49384 | The swap functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) ⇒ ⊢ (𝜑 → (𝐶 swapF 𝐷) ∈ (𝑆 Func 𝑇)) | ||
| Theorem | swapfiso 49385 | 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 49386 | The product category is categorically isomorphic to the swapped product category. (Contributed by Zhi Wang, 8-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑆 = (𝐶 ×c 𝐷) & ⊢ 𝑇 = (𝐷 ×c 𝐶) & ⊢ 𝐸 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑆( ≃𝑐 ‘𝐸)𝑇) | ||
| Theorem | oppc1stflem 49387* | 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 49388 | 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 49389 | 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 49390 | 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 49391 | 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 49392 | 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𝐷)) | ||
| Theorem | cofuswapfcl 49393 | 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 49394 | 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 49395 | 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 49396 | 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 49397 | 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 49398 | 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 49399* | 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 49400* | 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 ‘𝐹)⟨𝑧, 𝑌⟩)𝐾))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |