HomeTheorem List (p. 492 of 498)
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. 492 of 498) | < 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-30880) |
Hilbert Space Explorer
(30881-32403) |
Users' Mathboxes
(32404-49778) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | oppfrcl 49101 | If an opposite functor of a class is a functor, then the original class must be an ordered pair. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 & ⊢ 𝐺 = ( oppFunc ‘𝐹) ⇒ ⊢ (𝜑 → 𝐹 ∈ (V × V)) | ||
| Theorem | oppfrcl2 49102 | If an opposite functor of a class is a functor, then the two components of the original class must be sets. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 & ⊢ 𝐺 = ( oppFunc ‘𝐹) & ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩) ⇒ ⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
| Theorem | oppfrcl3 49103 | If an opposite functor of a class is a functor, then the second component of the original class must be a relation whose domain is a relation as well. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 & ⊢ 𝐺 = ( oppFunc ‘𝐹) & ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩) ⇒ ⊢ (𝜑 → (Rel 𝐵 ∧ Rel dom 𝐵)) | ||
| Theorem | oppf1st2nd 49104 | Rewrite the opposite functor into its components (eqopi 7967). (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 & ⊢ 𝐺 = ( oppFunc ‘𝐹) & ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩) ⇒ ⊢ (𝜑 → (𝐺 ∈ (V × V) ∧ ((1st ‘𝐺) = 𝐴 ∧ (2nd ‘𝐺) = tpos 𝐵))) | ||
| Theorem | 2oppf 49105 | The double opposite functor is the original functor. Remark 3.42 of [Adamek] p. 39. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 & ⊢ 𝐺 = ( oppFunc ‘𝐹) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐺) = 𝐹) | ||
| Theorem | eloppf 49106 | The pre-image of a non-empty opposite functor is non-empty; and the second component of the pre-image is a relation on triples. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ 𝐺 = ( oppFunc ‘𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝐹 ≠ ∅ ∧ (Rel (2nd ‘𝐹) ∧ Rel dom (2nd ‘𝐹)))) | ||
| Theorem | eloppf2 49107 | Both components of a pre-image of a non-empty opposite functor exist; and the second component is a relation on triples. (Contributed by Zhi Wang, 18-Nov-2025.) |
| ⊢ (𝐹 oppFunc 𝐺) = 𝐾 & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Rel 𝐺 ∧ Rel dom 𝐺))) | ||
| Theorem | oppfvallem 49108 | Lemma for oppfval 49109. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (Rel 𝐺 ∧ Rel dom 𝐺)) | ||
| Theorem | oppfval 49109 | Value of the opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 oppFunc 𝐺) = ⟨𝐹, tpos 𝐺⟩) | ||
| Theorem | oppfval2 49110 | Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → ( oppFunc ‘𝐹) = ⟨(1st ‘𝐹), tpos (2nd ‘𝐹)⟩) | ||
| Theorem | oppfval3 49111 | Value of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = ⟨𝐺, 𝐾⟩) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) = ⟨𝐺, tpos 𝐾⟩) | ||
| Theorem | oppf1 49112 | Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (1st ‘( oppFunc ‘𝐹)) = (1st ‘𝐹)) | ||
| Theorem | oppf2 49113 | Value of the morphism part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝑀(2nd ‘( oppFunc ‘𝐹))𝑁) = (𝑁(2nd ‘𝐹)𝑀)) | ||
| Theorem | oppfoppc 49114 | The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (𝐹 oppFunc 𝐺) ∈ (𝑂 Func 𝑃)) | ||
| Theorem | oppfoppc2 49115 | The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Func 𝑃)) | ||
| Theorem | funcoppc2 49116 | A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐹(𝑂 Func 𝑃)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)tpos 𝐺) | ||
| Theorem | funcoppc4 49117 | A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → (𝐹 oppFunc 𝐺) ∈ (𝑂 Func 𝑃)) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | ||
| Theorem | funcoppc5 49118 | A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Func 𝑃)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) | ||
| Theorem | 2oppffunc 49119 | The opposite functor of an opposite functor is a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025.) The functor in opposite categories does not have to be an opposite functor. (Revised by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑃)) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝐶 Func 𝐷)) | ||
| Theorem | funcoppc3 49120 | A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐹(𝑂 Func 𝑃)tpos 𝐺) & ⊢ (𝜑 → 𝐺 Fn (𝐴 × 𝐵)) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | ||
| Theorem | oppff1 49121 | The operation generating opposite functors is injective. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) ⇒ ⊢ ( oppFunc ↾ (𝐶 Func 𝐷)):(𝐶 Func 𝐷)–1-1→(𝑂 Func 𝑃) | ||
| Theorem | oppff1o 49122 | The operation generating opposite functors is bijective. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( oppFunc ↾ (𝐶 Func 𝐷)):(𝐶 Func 𝐷)–1-1-onto→(𝑂 Func 𝑃)) | ||
| Theorem | cofuoppf 49123 | Composition of opposite functors. (Contributed by Zhi Wang, 26-Nov-2025.) |
| ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (( oppFunc ‘𝐺) ∘func ( oppFunc ‘𝐹)) = ( oppFunc ‘𝐾)) | ||
| Theorem | imasubc 49124* | An image of a full functor is a full subcategory. Remark 4.2(3) of [Adamek] p. 48. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝐹(𝐷 Full 𝐸)𝐺) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐽 = (Homf ‘𝐸) ⇒ ⊢ (𝜑 → (𝐾 Fn (𝑆 × 𝑆) ∧ 𝑆 ⊆ 𝐶 ∧ (𝐽 ↾ (𝑆 × 𝑆)) = 𝐾)) | ||
| Theorem | imasubc2 49125* | An image of a full functor is a (full) subcategory. Remark 4.2(3) of [Adamek] p. 48. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝐹(𝐷 Full 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐸)) | ||
| Theorem | imassc 49126* | An image of a functor satisfies the subcategory subset relation. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ 𝐽 = (Homf ‘𝐸) ⇒ ⊢ (𝜑 → 𝐾 ⊆cat 𝐽) | ||
| Theorem | imaid 49127* | An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ 𝐼 = (Id‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐾𝑋)) | ||
| Theorem | imaf1co 49128* | An image of a functor whose object part is injective preserves the composition. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ ∙ = (comp‘𝐸) & ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐾𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐾𝑍)) ⇒ ⊢ (𝜑 → (𝑁(⟨𝑋, 𝑌⟩ ∙ 𝑍)𝑀) ∈ (𝑋𝐾𝑍)) | ||
| Theorem | imasubc3 49129* | An image of a functor injective on objects is a subcategory. Remark 4.2(3) of [Adamek] p. 48. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → Fun ◡𝐹) ⇒ ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐸)) | ||
| Theorem | fthcomf 49130* | Source categories of a faithful functor have the same base, hom-sets and composition operation if the composition is compatible in images of the functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐴 Faith 𝐶)𝐺) & ⊢ (𝜑 → 𝐹(𝐵 Func 𝐷)𝐺) & ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴) ∧ 𝑧 ∈ (Base‘𝐴))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐴)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐴)𝑧))) → (((𝑦𝐺𝑧)‘𝑔)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐶)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) ⇒ ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) | ||
| Theorem | idfth 49131 | The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸)) | ||
| Theorem | idemb 49132 | The inclusion functor is an embedding. Remark 4.4(1) in [Adamek] p. 49. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → (𝐼 ∈ (𝐷 Faith 𝐸) ∧ Fun ◡(1st ‘𝐼))) | ||
| Theorem | idsubc 49133 | The source category of an inclusion functor is a subcategory of the target category. See also Remark 4.4 in [Adamek] p. 49. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐷) ⇒ ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐻 ∈ (Subcat‘𝐸)) | ||
| Theorem | idfullsubc 49134 | The source category of an inclusion functor is a full subcategory of the target category if the inclusion functor is full. Remark 4.4(2) in [Adamek] p. 49. See also ressffth 17865. (Contributed by Zhi Wang, 11-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐷) & ⊢ 𝐽 = (Homf ‘𝐸) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝐼 ∈ (𝐷 Full 𝐸) → (𝐵 ⊆ 𝐶 ∧ (𝐽 ↾ (𝐵 × 𝐵)) = 𝐻)) | ||
| Theorem | cofidfth 49135 | If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then 𝐹 is faithful. Combined with cofidf1 49094, this theorem proves that 𝐹 is an embedding (a faithful functor injective on objects, remark 3.28(1) of [Adamek] p. 34). (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼) ⇒ ⊢ (𝜑 → 𝐹(𝐷 Faith 𝐸)𝐺) | ||
| Theorem | fulloppf 49136 | The opposite functor of a full functor is also full. Proposition 3.43(d) in [Adamek] p. 39. (Contributed by Zhi Wang, 26-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Full 𝐷)) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Full 𝑃)) | ||
| Theorem | fthoppf 49137 | The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in [Adamek] p. 39. (Contributed by Zhi Wang, 26-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Faith 𝐷)) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Faith 𝑃)) | ||
| Theorem | ffthoppf 49138 | The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Zhi Wang, 26-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ ((𝑂 Full 𝑃) ∩ (𝑂 Faith 𝑃))) | ||
| Theorem | upciclem1 49139* | Lemma for upcic 49143, upeu 49144, and upeu2 49145. (Contributed by Zhi Wang, 16-Sep-2025.) (Proof shortened by Zhi Wang, 5-Nov-2025.) |
| ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ (𝑍𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑛 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ∃!𝑙 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑙)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) | ||
| Theorem | upciclem2 49140 | Lemma for upciclem3 49141 and upeu2 49145. (Contributed by Zhi Wang, 19-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) ⇒ ⊢ (𝜑 → (((𝑋𝐺𝑍)‘(𝐿(⟨𝑋, 𝑌⟩ · 𝑍)𝐾))(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑍))𝑀) = (((𝑌𝐺𝑍)‘𝐿)(⟨𝑊, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))𝑁)) | ||
| Theorem | upciclem3 49141* | Lemma for upciclem4 49142. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑋)) & ⊢ (𝜑 → 𝑀 = (((𝑌𝐺𝑋)‘𝐿)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑋))𝑁)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) ⇒ ⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩ · 𝑋)𝐾) = ((Id‘𝐷)‘𝑋)) | ||
| Theorem | upciclem4 49142* | Lemma for upcic 49143 and upeu 49144. (Contributed by Zhi Wang, 19-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) & ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))) | ||
| Theorem | upcic 49143* | A universal property defines an object up to isomorphism given its existence. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) & ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)) ⇒ ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐷)𝑌) | ||
| Theorem | upeu 49144* | A universal property defines an essentially unique (strong form) pair of object 𝑋 and morphism 𝑀 if it exists. (Contributed by Zhi Wang, 19-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) & ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)) ⇒ ⊢ (𝜑 → ∃!𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) | ||
| Theorem | upeu2 49145* | Generate new universal morphism through isomorphism from existing universal object. (Contributed by Zhi Wang, 20-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ 𝐼 = (Iso‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)) ∧ ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))) | ||
| Syntax | cup 49146 | Extend class notation with the class of universal properties. |
| class UP | ||
| Definition | df-up 49147* |
Definition of the class of universal properties.
Given categories 𝐷 and 𝐸, if 𝐹:𝐷⟶𝐸 is a functor and 𝑊 an object of 𝐸, a universal pair from 𝑊 to 𝐹 is a pair ⟨𝑋, 𝑀⟩ consisting of an object 𝑋 of 𝐷 and a morphism 𝑀:𝑊⟶𝐹𝑋 of 𝐸, such that to every pair ⟨𝑦, 𝑔⟩ with 𝑦 an object of 𝐷 and 𝑔:𝑊⟶𝐹𝑦 a morphism of 𝐸, there is a unique morphism 𝑘:𝑋⟶𝑦 of 𝐷 with 𝐹𝑘 ⚬ 𝑀 = 𝑔. Such property is commonly referred to as a universal property. In our definition, it is denoted as 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀. Note that the universal pair is termed differently as "universal arrow" in p. 55 of Mac Lane, Saunders, Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf (retrieved 6 Oct 2025). Interestingly, the "universal arrow" is referring to the morphism 𝑀 instead of the pair near the end of the same piece of the text, causing name collision. The name "universal arrow" is also adopted in papers such as https://arxiv.org/pdf/2212.08981. Alternatively, the universal pair is called the "universal morphism" in Wikipedia (https://en.wikipedia.org/wiki/Universal_property) as well as published works, e.g., https://arxiv.org/pdf/2412.12179. But the pair ⟨𝑋, 𝑀⟩ should be named differently as the morphism 𝑀, and thus we call 𝑋 the universal object, 𝑀 the universal morphism, and ⟨𝑋, 𝑀⟩ the universal pair. Given its existence, such universal pair is essentially unique (upeu3 49168), and can be generated from an existing universal pair by isomorphisms (upeu4 49169). See also oppcup 49180 for the dual concept. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ UP = (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})) | ||
| Theorem | reldmup 49148 | The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ Rel dom UP | ||
| Theorem | upfval 49149* | Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.) (Proof shortened by Zhi Wang, 12-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) ⇒ ⊢ (𝐷 UP 𝐸) = (𝑓 ∈ (𝐷 Func 𝐸), 𝑤 ∈ 𝐶 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑤𝐽((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑤𝐽((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑂((1st ‘𝑓)‘𝑦))𝑚))}) | ||
| Theorem | upfval2 49150* | Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝐹(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽((1st ‘𝐹)‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽((1st ‘𝐹)‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥(2nd ‘𝐹)𝑦)‘𝑘)(⟨𝑊, ((1st ‘𝐹)‘𝑥)⟩𝑂((1st ‘𝐹)‘𝑦))𝑚))}) | ||
| Theorem | upfval3 49151* | Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽(𝐹‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑥)⟩𝑂(𝐹‘𝑦))𝑚))}) | ||
| Theorem | isuplem 49152* | Lemma for isup 49153 and other theorems. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)))) | ||
| Theorem | isup 49153* | The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ⇒ ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))) | ||
| Theorem | uppropd 49154 | If two categories have the same set of objects, morphisms, and compositions, then they have the same universal pairs. (Contributed by Zhi Wang, 20-Nov-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 UP 𝐶) = (𝐵 UP 𝐷)) | ||
| Theorem | reldmup2 49155 | The domain of (𝐷 UP 𝐸) is a relation. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ Rel dom (𝐷 UP 𝐸) | ||
| Theorem | relup 49156 | The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ Rel (𝐹(𝐷 UP 𝐸)𝑊) | ||
| Theorem | uprcl 49157 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝑊 ∈ 𝐶)) | ||
| Theorem | up1st2nd 49158 | Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀) | ||
| Theorem | up1st2ndr 49159 | Combine separated parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀) | ||
| Theorem | up1st2ndb 49160 | Combine/separate parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀 ↔ 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)) | ||
| Theorem | up1st2nd2 49161 | Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊)) ⇒ ⊢ (𝜑 → (1st ‘𝑋)(𝐹(𝐷 UP 𝐸)𝑊)(2nd ‘𝑋)) | ||
| Theorem | uprcl2 49162 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) | ||
| Theorem | uprcl3 49163 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝑊 ∈ 𝐶) | ||
| Theorem | uprcl4 49164 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) & ⊢ 𝐵 = (Base‘𝐷) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | uprcl5 49165 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) & ⊢ 𝐽 = (Hom ‘𝐸) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) | ||
| Theorem | uobrcl 49166 | Reverse closure for universal object. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝑋 ∈ dom (𝐹(𝐷 UP 𝐸)𝑊) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) | ||
| Theorem | isup2 49167* | The universal property of a universal pair. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)) | ||
| Theorem | upeu3 49168* | The universal pair ⟨𝑋, 𝑀⟩ from object 𝑊 to functor ⟨𝐹, 𝐺⟩ is essentially unique (strong form) if it exists. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ (𝜑 → 𝐼 = (Iso‘𝐷)) & ⊢ (𝜑 → ⚬ = (⟨𝑊, (𝐹‘𝑋)⟩(comp‘𝐸)(𝐹‘𝑌))) & ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) & ⊢ (𝜑 → 𝑌(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑁) ⇒ ⊢ (𝜑 → ∃!𝑟 ∈ (𝑋𝐼𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟) ⚬ 𝑀)) | ||
| Theorem | upeu4 49169 | Generate a new universal morphism through an isomorphism from an existing universal object, and pair with the codomain of the isomorphism to form a universal pair. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝐼 = (Iso‘𝐷)) & ⊢ (𝜑 → ⚬ = (⟨𝑊, (𝐹‘𝑋)⟩(comp‘𝐸)(𝐹‘𝑌))) & ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾) ⚬ 𝑀)) ⇒ ⊢ (𝜑 → 𝑌(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑁) | ||
| Theorem | uptposlem 49170 | Lemma for uptpos 49171. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ (𝜑 → tpos 𝐺 = 𝐻) ⇒ ⊢ (𝜑 → tpos 𝐻 = 𝐺) | ||
| Theorem | uptpos 49171 | Rewrite the predicate of universal property in the form of opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ (𝜑 → tpos 𝐺 = 𝐻) ⇒ ⊢ (𝜑 → 𝑋(⟨𝐹, tpos 𝐻⟩(𝑂 UP 𝑃)𝑊)𝑀) | ||
| Theorem | oppcuprcl4 49172 | Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝑂 = (oppCat‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | oppcuprcl3 49173 | Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝑃 = (oppCat‘𝐸) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝑊 ∈ 𝐶) | ||
| Theorem | oppcuprcl5 49174 | Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝑃 = (oppCat‘𝐸) & ⊢ 𝐽 = (Hom ‘𝐸) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐹‘𝑋)𝐽𝑊)) | ||
| Theorem | oppcuprcl2 49175 | 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 49176 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(𝐺(𝑂 UP 𝑃)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑃)) | ||
| Theorem | oppfuprcl 49177 | 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 49178 | 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 49179* | Lemma for oppcup3 49182. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ ((𝐹‘𝑦)𝐽𝑍)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑛 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩𝑂𝑍)((𝑦𝐺𝑋)‘𝑘))) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ((𝐹‘𝑌)𝐽𝑍)) ⇒ ⊢ (𝜑 → ∃!𝑙 ∈ (𝑌𝐻𝑋)𝑁 = (𝑀(⟨(𝐹‘𝑌), (𝐹‘𝑋)⟩𝑂𝑍)((𝑌𝐺𝑋)‘𝑙))) | ||
| Theorem | oppcup 49180* | 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 49181* | 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 49182* | 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 49183* | Lemma for uptr 49186. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ ∙ = (comp‘𝐷) & ⊢ ⚬ = (comp‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷)) & ⊢ (𝜑 → (𝑀‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝐹‘𝑍))) & ⊢ (𝜑 → ((𝑋𝑁(𝐹‘𝑍))‘𝐴) = 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝑀((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑁) & ⊢ (𝜑 → (⟨𝑀, 𝑁⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) ⇒ ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽(𝐾‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ ∀𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴))) | ||
| Theorem | uptrlem2 49184* | Lemma for uptr 49186. (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 49185 | Lemma for uptr 49186. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptr 49186 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍))) ⇒ ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptri 49187 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uptra 49188 | 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 49189 | 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 49190 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uobffth 49191 | 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 49192 | 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 49193 | 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 49194 | 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 49195 | 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 49196* | 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 49197 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | ||
| Theorem | natrcl3 49198 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) | ||
| Theorem | catbas 49199 | The base of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ 𝐵 ∈ V ⇒ ⊢ 𝐵 = (Base‘𝐶) | ||
| Theorem | cathomfval 49200 | The hom-sets of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} & ⊢ 𝐻 ∈ V ⇒ ⊢ 𝐻 = (Hom ‘𝐶) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |