HomeTheorem List (p. 497 of 503)
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. 497 of 503) | < 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-30989) |
Hilbert Space Explorer
(30990-32512) |
Users' Mathboxes
(32513-50280) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | oppfvalg 49601 | Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 oppFunc 𝐺) = if((Rel 𝐺 ∧ Rel dom 𝐺), ⟨𝐹, tpos 𝐺⟩, ∅)) | ||
| Theorem | oppfrcllem 49602 | Lemma for oppfrcl 49603. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 ⇒ ⊢ (𝜑 → 𝐺 ≠ ∅) | ||
| Theorem | oppfrcl 49603 | 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 49604 | 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 49605 | 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 49606 | Rewrite the opposite functor into its components (eqopi 7978). (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 & ⊢ 𝐺 = ( oppFunc ‘𝐹) & ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩) ⇒ ⊢ (𝜑 → (𝐺 ∈ (V × V) ∧ ((1st ‘𝐺) = 𝐴 ∧ (2nd ‘𝐺) = tpos 𝐵))) | ||
| Theorem | 2oppf 49607 | 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 49608 | 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 49609 | 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 49610 | Lemma for oppfval 49611. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (Rel 𝐺 ∧ Rel dom 𝐺)) | ||
| Theorem | oppfval 49611 | Value of the opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 oppFunc 𝐺) = ⟨𝐹, tpos 𝐺⟩) | ||
| Theorem | oppfval2 49612 | Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → ( oppFunc ‘𝐹) = ⟨(1st ‘𝐹), tpos (2nd ‘𝐹)⟩) | ||
| Theorem | oppfval3 49613 | Value of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = ⟨𝐺, 𝐾⟩) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) = ⟨𝐺, tpos 𝐾⟩) | ||
| Theorem | oppf1 49614 | Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (1st ‘( oppFunc ‘𝐹)) = (1st ‘𝐹)) | ||
| Theorem | oppf2 49615 | Value of the morphism part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝑀(2nd ‘( oppFunc ‘𝐹))𝑁) = (𝑁(2nd ‘𝐹)𝑀)) | ||
| Theorem | oppfoppc 49616 | The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (𝐹 oppFunc 𝐺) ∈ (𝑂 Func 𝑃)) | ||
| Theorem | oppfoppc2 49617 | The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Func 𝑃)) | ||
| Theorem | funcoppc2 49618 | 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 49619 | 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 49620 | 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 49621 | 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 49622 | 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 49623 | The operation generating opposite functors is injective. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) ⇒ ⊢ ( oppFunc ↾ (𝐶 Func 𝐷)):(𝐶 Func 𝐷)–1-1→(𝑂 Func 𝑃) | ||
| Theorem | oppff1o 49624 | 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 49625 | Composition of opposite functors. (Contributed by Zhi Wang, 26-Nov-2025.) |
| ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (( oppFunc ‘𝐺) ∘func ( oppFunc ‘𝐹)) = ( oppFunc ‘𝐾)) | ||
| Theorem | imasubc 49626* | 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 49627* | 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 49628* | An image of a functor satisfies the subcategory subset relation. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ 𝐽 = (Homf ‘𝐸) ⇒ ⊢ (𝜑 → 𝐾 ⊆cat 𝐽) | ||
| Theorem | imaid 49629* | An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ 𝐼 = (Id‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐾𝑋)) | ||
| Theorem | imaf1co 49630* | 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 49631* | 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 49632* | 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 49633 | The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸)) | ||
| Theorem | idemb 49634 | 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 49635 | 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 49636 | 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 17907. (Contributed by Zhi Wang, 11-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐷) & ⊢ 𝐽 = (Homf ‘𝐸) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝐼 ∈ (𝐷 Full 𝐸) → (𝐵 ⊆ 𝐶 ∧ (𝐽 ↾ (𝐵 × 𝐵)) = 𝐻)) | ||
| Theorem | cofidfth 49637 | If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then 𝐹 is faithful. Combined with cofidf1 49596, 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 49638 | 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 49639 | 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 49640 | 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 49641* | Lemma for upcic 49645, upeu 49646, and upeu2 49647. (Contributed by Zhi Wang, 16-Sep-2025.) (Proof shortened by Zhi Wang, 5-Nov-2025.) |
| ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ (𝑍𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑛 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ∃!𝑙 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑙)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) | ||
| Theorem | upciclem2 49642 | Lemma for upciclem3 49643 and upeu2 49647. (Contributed by Zhi Wang, 19-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) ⇒ ⊢ (𝜑 → (((𝑋𝐺𝑍)‘(𝐿(⟨𝑋, 𝑌⟩ · 𝑍)𝐾))(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑍))𝑀) = (((𝑌𝐺𝑍)‘𝐿)(⟨𝑊, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))𝑁)) | ||
| Theorem | upciclem3 49643* | Lemma for upciclem4 49644. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑋)) & ⊢ (𝜑 → 𝑀 = (((𝑌𝐺𝑋)‘𝐿)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑋))𝑁)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) ⇒ ⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩ · 𝑋)𝐾) = ((Id‘𝐷)‘𝑋)) | ||
| Theorem | upciclem4 49644* | Lemma for upcic 49645 and upeu 49646. (Contributed by Zhi Wang, 19-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) & ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))) | ||
| Theorem | upcic 49645* | 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 49646* | 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 49647* | 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 49648 | Extend class notation with the class of universal properties. |
| class UP | ||
| Definition | df-up 49649* |
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 49670), and can be generated from an existing universal pair by isomorphisms (upeu4 49671). See also oppcup 49682 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 49650 | The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ Rel dom UP | ||
| Theorem | upfval 49651* | 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 49652* | 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 49653* | Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽(𝐹‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑥)⟩𝑂(𝐹‘𝑦))𝑚))}) | ||
| Theorem | isuplem 49654* | Lemma for isup 49655 and other theorems. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)))) | ||
| Theorem | isup 49655* | The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ⇒ ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))) | ||
| Theorem | uppropd 49656 | 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 49657 | The domain of (𝐷 UP 𝐸) is a relation. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ Rel dom (𝐷 UP 𝐸) | ||
| Theorem | relup 49658 | The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ Rel (𝐹(𝐷 UP 𝐸)𝑊) | ||
| Theorem | uprcl 49659 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝑊 ∈ 𝐶)) | ||
| Theorem | up1st2nd 49660 | Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀) | ||
| Theorem | up1st2ndr 49661 | Combine separated parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀) | ||
| Theorem | up1st2ndb 49662 | Combine/separate parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀 ↔ 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)) | ||
| Theorem | up1st2nd2 49663 | Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊)) ⇒ ⊢ (𝜑 → (1st ‘𝑋)(𝐹(𝐷 UP 𝐸)𝑊)(2nd ‘𝑋)) | ||
| Theorem | uprcl2 49664 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) | ||
| Theorem | uprcl3 49665 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝑊 ∈ 𝐶) | ||
| Theorem | uprcl4 49666 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) & ⊢ 𝐵 = (Base‘𝐷) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | uprcl5 49667 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) & ⊢ 𝐽 = (Hom ‘𝐸) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) | ||
| Theorem | uobrcl 49668 | Reverse closure for universal object. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ (𝑋 ∈ dom (𝐹(𝐷 UP 𝐸)𝑊) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) | ||
| Theorem | isup2 49669* | The universal property of a universal pair. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)) | ||
| Theorem | upeu3 49670* | 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 49671 | 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 49672 | Lemma for uptpos 49673. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ (𝜑 → tpos 𝐺 = 𝐻) ⇒ ⊢ (𝜑 → tpos 𝐻 = 𝐺) | ||
| Theorem | uptpos 49673 | 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 49674 | Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝑂 = (oppCat‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | oppcuprcl3 49675 | Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝑃 = (oppCat‘𝐸) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝑊 ∈ 𝐶) | ||
| Theorem | oppcuprcl5 49676 | Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀) & ⊢ 𝑃 = (oppCat‘𝐸) & ⊢ 𝐽 = (Hom ‘𝐸) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐹‘𝑋)𝐽𝑊)) | ||
| Theorem | oppcuprcl2 49677 | 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 49678 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝑋(𝐺(𝑂 UP 𝑃)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑃)) | ||
| Theorem | oppfuprcl 49679 | 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 49680 | 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 49681* | Lemma for oppcup3 49684. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ ((𝐹‘𝑦)𝐽𝑍)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑛 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩𝑂𝑍)((𝑦𝐺𝑋)‘𝑘))) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ((𝐹‘𝑌)𝐽𝑍)) ⇒ ⊢ (𝜑 → ∃!𝑙 ∈ (𝑌𝐻𝑋)𝑁 = (𝑀(⟨(𝐹‘𝑌), (𝐹‘𝑋)⟩𝑂𝑍)((𝑌𝐺𝑋)‘𝑙))) | ||
| Theorem | oppcup 49682* | 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 49683* | 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 49684* | 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 49685* | Lemma for uptr 49688. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ ∙ = (comp‘𝐷) & ⊢ ⚬ = (comp‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐷)) & ⊢ (𝜑 → (𝑀‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝐹‘𝑍))) & ⊢ (𝜑 → ((𝑋𝑁(𝐹‘𝑍))‘𝐴) = 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝑀((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑁) & ⊢ (𝜑 → (⟨𝑀, 𝑁⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) ⇒ ⊢ (𝜑 → (∀ℎ ∈ (𝑌𝐽(𝐾‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)ℎ = (((𝑍𝐿𝑊)‘𝑘)(⟨𝑌, (𝐾‘𝑍)⟩ ⚬ (𝐾‘𝑊))𝐵) ↔ ∀𝑔 ∈ (𝑋𝐼(𝐹‘𝑊))∃!𝑘 ∈ (𝑍𝐻𝑊)𝑔 = (((𝑍𝐺𝑊)‘𝑘)(⟨𝑋, (𝐹‘𝑍)⟩ ∙ (𝐹‘𝑊))𝐴))) | ||
| Theorem | uptrlem2 49686* | Lemma for uptr 49688. (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 49687 | Lemma for uptr 49688. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptr 49688 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐽(𝐹‘𝑍))) ⇒ ⊢ (𝜑 → (𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀 ↔ 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁)) | ||
| Theorem | uptri 49689 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → (𝑅‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝑅((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))𝑆) & ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝐾, 𝐿⟩) & ⊢ (𝜑 → ((𝑋𝑆(𝐹‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(⟨𝐹, 𝐺⟩(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(⟨𝐾, 𝐿⟩(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uptra 49690 | 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 49691 | 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 49692 | Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → ((1st ‘𝐾)‘𝑋) = 𝑌) & ⊢ (𝜑 → 𝐾 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) & ⊢ (𝜑 → (𝐾 ∘func 𝐹) = 𝐺) & ⊢ (𝜑 → ((𝑋(2nd ‘𝐾)((1st ‘𝐹)‘𝑍))‘𝑀) = 𝑁) & ⊢ (𝜑 → 𝑍(𝐹(𝐶 UP 𝐷)𝑋)𝑀) ⇒ ⊢ (𝜑 → 𝑍(𝐺(𝐶 UP 𝐸)𝑌)𝑁) | ||
| Theorem | uobffth 49693 | 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 49694 | 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 49695 | 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 49696 | 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 49697 | 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 49698* | 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 49699 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | ||
| Theorem | natrcl3 49700 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |