HomeTheorem List (p. 497 of 504)
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 504) | < 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-31056) |
Hilbert Space Explorer
(31057-32579) |
Users' Mathboxes
(32580-50364) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cicfn 49601 | ≃𝑐 is a function on Cat. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ ≃𝑐 Fn Cat | ||
| Theorem | cicrcl2 49602 | Isomorphism implies the structure being a category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 → 𝐶 ∈ Cat) | ||
| Theorem | oppccic 49603 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝐶)𝑆) ⇒ ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | relcic 49604 | The set of isomorphic objects is a relation. Simplifies cicer 17811 (see cicerALT 49605). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → Rel ( ≃𝑐 ‘𝐶)) | ||
| Theorem | cicerALT 49605 | Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in [Adamek] p. 29. (Contributed by AV, 5-Apr-2020.) (Proof shortened by Zhi Wang, 3-Nov-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) Er (Base‘𝐶)) | ||
| Theorem | cic1st2nd 49606 | Reconstruction of a pair of isomorphic objects in terms of its ordered pair components. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝑃 ∈ ( ≃𝑐 ‘𝐶) → 𝑃 = ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩) | ||
| Theorem | cic1st2ndbr 49607 | Rewrite the predicate of isomorphic objects with separated parts. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝑃 ∈ ( ≃𝑐 ‘𝐶) → (1st ‘𝑃)( ≃𝑐 ‘𝐶)(2nd ‘𝑃)) | ||
| Theorem | cicpropdlem 49608 | Lemma for cicpropd 49609. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘𝐶)) → 𝑃 ∈ ( ≃𝑐 ‘𝐷)) | ||
| Theorem | cicpropd 49609 | Two structures with the same base, hom-sets and composition operation have the same isomorphic objects. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → ( ≃𝑐 ‘𝐶) = ( ≃𝑐 ‘𝐷)) | ||
| Theorem | oppccicb 49610 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 ↔ 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | oppcciceq 49611 | The opposite category has the same isomorphic objects as the original category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ ( ≃𝑐 ‘𝐶) = ( ≃𝑐 ‘𝑂) | ||
| Theorem | dmdm 49612 | The double domain of a function on a Cartesian square. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ (𝐴 Fn (𝐵 × 𝐵) → 𝐵 = dom dom 𝐴) | ||
| Theorem | iinfssclem1 49613* | Lemma for iinfssc 49616. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 = (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝑆, 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 ↦ ∩ 𝑥 ∈ 𝐴 (𝑧𝐻𝑤))) | ||
| Theorem | iinfssclem2 49614* | Lemma for iinfssc 49616. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆)) | ||
| Theorem | iinfssclem3 49615* | Lemma for iinfssc 49616. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = ∩ 𝑥 ∈ 𝐴 (𝑋𝐻𝑌)) | ||
| Theorem | iinfssc 49616* | Indexed intersection of subcategories is a subcategory (the category-agnostic version). (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ⊆cat 𝐽) | ||
| Theorem | iinfsubc 49617* | Indexed intersection of subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶)) | ||
| Theorem | iinfprg 49618* | Indexed intersection of functions with an unordered pair index. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) = (𝑥 ∈ ∩ 𝑦 ∈ {𝐴, 𝐵}dom 𝑦 ↦ ∩ 𝑦 ∈ {𝐴, 𝐵} (𝑦‘𝑥))) | ||
| Theorem | infsubc 49619* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ (Subcat‘𝐶) ∧ 𝐵 ∈ (Subcat‘𝐶)) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) ∈ (Subcat‘𝐶)) | ||
| Theorem | infsubc2 49620* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ (Subcat‘𝐶) ∧ 𝐵 ∈ (Subcat‘𝐶)) → (𝑥 ∈ (dom dom 𝐴 ∩ dom dom 𝐵), 𝑦 ∈ (dom dom 𝐴 ∩ dom dom 𝐵) ↦ ((𝑥𝐴𝑦) ∩ (𝑥𝐵𝑦))) ∈ (Subcat‘𝐶)) | ||
| Theorem | infsubc2d 49621* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑇), 𝑦 ∈ (𝑆 ∩ 𝑇) ↦ ((𝑥𝐻𝑦) ∩ (𝑥𝐽𝑦))) ∈ (Subcat‘𝐶)) | ||
| Theorem | discsubclem 49622* | Lemma for discsubc 49623. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) ⇒ ⊢ 𝐽 Fn (𝑆 × 𝑆) | ||
| Theorem | discsubc 49623* | A discrete category, whose only morphisms are the identity morphisms, is a subcategory. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) | ||
| Theorem | iinfconstbaslem 49624* | Lemma for iinfconstbas 49625. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 = ((Subcat‘𝐶) ∩ {𝑗 ∣ 𝑗 Fn (𝑆 × 𝑆)})) ⇒ ⊢ (𝜑 → 𝐽 ∈ 𝐴) | ||
| Theorem | iinfconstbas 49625* | The discrete category is the indexed intersection of all subcategories with the same base. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 = ((Subcat‘𝐶) ∩ {𝑗 ∣ 𝑗 Fn (𝑆 × 𝑆)})) ⇒ ⊢ (𝜑 → 𝐽 = (𝑧 ∈ ∩ ℎ ∈ 𝐴 dom ℎ ↦ ∩ ℎ ∈ 𝐴 (ℎ‘𝑧))) | ||
| Theorem | nelsubclem 49626* | Lemma for nelsubc 49627. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ 𝐻 = (Homf ‘𝐶) ⇒ ⊢ (𝜑 → (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat 𝐻 ∧ (¬ ∀𝑥 ∈ 𝑆 𝐼 ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)𝜓)))) | ||
| Theorem | nelsubc 49627* | An empty "hom-set" for non-empty base satisfies all conditions for a subcategory but the existence of identity morphisms. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat 𝐻 ∧ (¬ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) | ||
| Theorem | nelsubc2 49628 | An empty "hom-set" for non-empty base is not a subcategory. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → ¬ 𝐽 ∈ (Subcat‘𝐶)) | ||
| Theorem | nelsubc3lem 49629* | Lemma for nelsubc3 49630. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 ∈ Cat & ⊢ 𝐽 ∈ V & ⊢ 𝑆 ∈ V & ⊢ (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))) ⇒ ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) | ||
| Theorem | nelsubc3 49630* |
Remark 4.2(2) of [Adamek] p. 48. There exists
a set satisfying all
conditions for a subcategory but the existence of identity morphisms.
Therefore such condition in df-subc 17817 is necessary.
Note that this theorem cheated a little bit because (𝐶 ↾cat 𝐽) is not a category. In fact (𝐶 ↾cat 𝐽) ∈ Cat is a stronger statement than the condition (d) of Definition 4.1(1) of [Adamek] p. 48, as stated here (see the proof of issubc3 17854). To construct such a category, see setc1onsubc 50161 and cnelsubc 50163. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) | ||
| Theorem | ssccatid 49631* | A category 𝐶 restricted by 𝐽 is a category if all of the following are satisfied: a) the base is a subset of base of 𝐶, b) all hom-sets are subsets of hom-sets of 𝐶, c) it has identity morphisms for all objects, d) the composition under 𝐶 is closed in 𝐽. But 𝐽 might not be a subcategory of 𝐶 (see cnelsubc 50163). (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐽 ⊆cat 𝐻) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 1 ∈ (𝑦𝐽𝑦)) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ (𝑎𝐽𝑏))) → ( 1 (⟨𝑎, 𝑏⟩ · 𝑏)𝑚) = 𝑚) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ (𝑎𝐽𝑏))) → (𝑚(⟨𝑎, 𝑎⟩ · 𝑏) 1 ) = 𝑚) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐽𝑧)) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑦 ∈ 𝑆 ↦ 1 ))) | ||
| Theorem | resccatlem 49632* | Lemma for resccat 49633. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑆 = (Base‘𝐸) & ⊢ 𝐽 = (Homf ‘𝐸) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐸) & ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ↔ 𝐸 ∈ Cat)) | ||
| Theorem | resccat 49633* | A class 𝐶 restricted by the hom-sets of another set 𝐸, whose base is a subset of the base of 𝐶 and whose composition is compatible with 𝐶, is a category iff 𝐸 is a category. Note that the compatibility condition "resccat.1" can be weakened by removing 𝑥 ∈ 𝑆 because 𝑓 ∈ (𝑥𝐽𝑦) implies these. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑆 = (Base‘𝐸) & ⊢ 𝐽 = (Homf ‘𝐸) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐸) & ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ↔ 𝐸 ∈ Cat)) | ||
| Theorem | reldmfunc 49634 | The domain of Func is a relation. (Contributed by Zhi Wang, 12-Nov-2025.) |
| ⊢ Rel dom Func | ||
| Theorem | func1st2nd 49635 | Rewrite the functor predicate with separated parts. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | ||
| Theorem | func1st 49636 | Extract the first member of a functor. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹) | ||
| Theorem | func2nd 49637 | Extract the second member of a functor. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺) | ||
| Theorem | funcrcl2 49638 | Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
| Theorem | funcrcl3 49639 | Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐸 ∈ Cat) | ||
| Theorem | funcf2lem 49640* | A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | funcf2lem2 49641* | A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = (𝐸‘𝐶) ⇒ ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | 0funcglem 49642 | Lemma for 0funcg 49644. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ (𝜑 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → (𝜃 ↔ 𝜁)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜂 ∧ 𝜁))) | ||
| Theorem | 0funcg2 49643 | The functor from the empty category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ∅ = (Base‘𝐶)) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ (𝐹 = ∅ ∧ 𝐺 = ∅))) | ||
| Theorem | 0funcg 49644 | The functor from the empty category. Corollary of Definition 3.47 of [Adamek] p. 40, Definition 7.1 of [Adamek] p. 101, Example 3.3(4.c) of [Adamek] p. 24, and Example 7.2(3) of [Adamek] p. 101. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ∅ = (Base‘𝐶)) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐶 Func 𝐷) = {⟨∅, ∅⟩}) | ||
| Theorem | 0funclem 49645 | Lemma for 0funcALT 49647. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ (𝜒 ↔ 𝜂) & ⊢ (𝜃 ↔ 𝜁) & ⊢ 𝜏 ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜂 ∧ 𝜁))) | ||
| Theorem | 0func 49646 | The functor from the empty category. (Contributed by Zhi Wang, 7-Oct-2025.) (Proof shortened by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (∅ Func 𝐶) = {⟨∅, ∅⟩}) | ||
| Theorem | 0funcALT 49647 | Alternate proof of 0func 49646. (Contributed by Zhi Wang, 7-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (∅ Func 𝐶) = {⟨∅, ∅⟩}) | ||
| Theorem | func0g 49648 | The source category of a functor to the empty category must be empty as well. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐵 = ∅) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
| Theorem | func0g2 49649 | The source category of a functor to the empty category must be empty as well. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐵 = ∅) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
| Theorem | initc 49650* | Sets with empty base are the only initial objects in the category of small categories. Example 7.2(3) of [Adamek] p. 101. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ ((𝐶 ∈ V ∧ ∅ = (Base‘𝐶)) ↔ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑)) | ||
| Theorem | cofu1st2nd 49651 | Rewrite the functor composition with separated functor parts. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) = (⟨(1st ‘𝐺), (2nd ‘𝐺)⟩ ∘func ⟨(1st ‘𝐹), (2nd ‘𝐹)⟩)) | ||
| Theorem | rescofuf 49652 | The restriction of functor composition is a function from product functor space to functor space. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ ( ∘func ↾ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))):((𝐷 Func 𝐸) × (𝐶 Func 𝐷))⟶(𝐶 Func 𝐸) | ||
| Theorem | cofu1a 49653 | Value of the object part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = (𝑀‘𝑋)) | ||
| Theorem | cofu2a 49654 | Value of the morphism part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑋𝑁𝑌)‘𝑅)) | ||
| Theorem | cofucla 49655 | The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) ⇒ ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) ∈ (𝐶 Func 𝐸)) | ||
| Theorem | funchomf 49656 | Source categories of a functor have the same set of objects and morphisms. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐴 Func 𝐶)𝐺) & ⊢ (𝜑 → 𝐹(𝐵 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) | ||
| Theorem | idfurcl 49657 | Reverse closure for an identity functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ ((idfunc‘𝐶) ∈ (𝐷 Func 𝐸) → 𝐶 ∈ Cat) | ||
| Theorem | idfu1stf1o 49658 | The identity functor/inclusion functor is bijective on objects. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → (1st ‘𝐼):𝐵–1-1-onto→𝐵) | ||
| Theorem | idfu1stalem 49659 | Lemma for idfu1sta 49660. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐷)) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
| Theorem | idfu1sta 49660 | Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐷)) ⇒ ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵)) | ||
| Theorem | idfu1a 49661 | Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋) | ||
| Theorem | idfu2nda 49662 | Value of the morphism part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (𝑋(Hom ‘𝐷)𝑌)) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ 𝐻)) | ||
| Theorem | imasubclem1 49663* | Lemma for imasubc 49710. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷) ∈ V) | ||
| Theorem | imasubclem2 49664* | Lemma for imasubc 49710. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ 𝐾 = (𝑦 ∈ 𝑋, 𝑧 ∈ 𝑌 ↦ ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷)) ⇒ ⊢ (𝜑 → 𝐾 Fn (𝑋 × 𝑌)) | ||
| Theorem | imasubclem3 49665* | Lemma for imasubc 49710. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐾 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ∪ 𝑧 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐺 “ {𝑦}))((𝐻‘𝐶) “ 𝐷)) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = ∪ 𝑧 ∈ ((◡𝐹 “ {𝑋}) × (◡𝐺 “ {𝑌}))((𝐻‘𝐶) “ 𝐷)) | ||
| Theorem | imaf1homlem 49666 | Lemma for imaf1hom 49667 and other theorems. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → ({(◡𝐹‘𝑋)} = (◡𝐹 “ {𝑋}) ∧ (𝐹‘(◡𝐹‘𝑋)) = 𝑋 ∧ (◡𝐹‘𝑋) ∈ 𝐵)) | ||
| Theorem | imaf1hom 49667* | The hom-set of an image of a functor injective on objects. (Contributed by Zhi Wang, 7-Nov-2025.) |
| ⊢ 𝑆 = (𝐹 “ 𝐴) & ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝))) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = (((◡𝐹‘𝑋)𝐺(◡𝐹‘𝑌)) “ ((◡𝐹‘𝑋)𝐻(◡𝐹‘𝑌)))) | ||
| Theorem | imaidfu2lem 49668 | Lemma for imaidfu2 49670. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → ((1st ‘𝐼) “ (Base‘𝐷)) = (Base‘𝐷)) | ||
| Theorem | imaidfu 49669* | The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸)) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Homf ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝))) & ⊢ 𝑆 = ((1st ‘𝐼) “ 𝐴) ⇒ ⊢ (𝜑 → (𝐽 ↾ (𝑆 × 𝑆)) = 𝐾) | ||
| Theorem | imaidfu2 49670* | The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐶) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸)) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Homf ‘𝐷) & ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝))) & ⊢ (𝜑 → 𝑆 = (Base‘𝐷)) ⇒ ⊢ (𝜑 → 𝐽 = 𝐾) | ||
| Theorem | cofid1a 49671 | Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷)) & ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼) ⇒ ⊢ (𝜑 → ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑋)) = 𝑋) | ||
| Theorem | cofid2a 49672 | Express the morphism part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷)) & ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌))‘((𝑋(2nd ‘𝐹)𝑌)‘𝑅)) = 𝑅) | ||
| Theorem | cofid1 49673 | Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼) ⇒ ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = 𝑋) | ||
| Theorem | cofid2 49674 | Express the morphism part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = 𝑅) | ||
| Theorem | cofidvala 49675* | The property "𝐹 is a section of 𝐺 " in a category of small categories (in a universe); expressed explicitly. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷)) & ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼) & ⊢ 𝐻 = (Hom ‘𝐷) ⇒ ⊢ (𝜑 → (((1st ‘𝐺) ∘ (1st ‘𝐹)) = ( I ↾ 𝐵) ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) = (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧))))) | ||
| Theorem | cofidf2a 49676 | If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then the morphism part of 𝐹 is injective, and the morphism part of 𝐺 is surjective in the image of 𝐹. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷)) & ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐹)𝑌):(𝑋𝐻𝑌)–1-1→(((1st ‘𝐹)‘𝑋)𝐽((1st ‘𝐹)‘𝑌)) ∧ (((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)):(((1st ‘𝐹)‘𝑋)𝐽((1st ‘𝐹)‘𝑌))–onto→(𝑋𝐻𝑌))) | ||
| Theorem | cofidf1a 49677 | If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then the object part of 𝐹 is injective, and the object part of 𝐺 is surjective. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷)) & ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝜑 → ((1st ‘𝐹):𝐵–1-1→𝐶 ∧ (1st ‘𝐺):𝐶–onto→𝐵)) | ||
| Theorem | cofidval 49678* | The property "⟨𝐹, 𝐺⟩ is a section of ⟨𝐾, 𝐿⟩ " in a category of small categories (in a universe); expressed explicitly. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼) & ⊢ 𝐻 = (Hom ‘𝐷) ⇒ ⊢ (𝜑 → ((𝐾 ∘ 𝐹) = ( I ↾ 𝐵) ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐿(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦))) = (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧))))) | ||
| Theorem | cofidf2 49679 | If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then the morphism part of 𝐹 is injective, and the morphism part of 𝐺 is surjective in the image of 𝐹. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌):(𝑋𝐻𝑌)–1-1→((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ∧ ((𝐹‘𝑋)𝐿(𝐹‘𝑌)):((𝐹‘𝑋)𝐽(𝐹‘𝑌))–onto→(𝑋𝐻𝑌))) | ||
| Theorem | cofidf1 49680 | If "⟨𝐹, 𝐺⟩ is a section of ⟨𝐾, 𝐿⟩ " in a category of small categories (in a universe), then 𝐹 is injective, and 𝐾 is surjective. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ 𝐼 = (idfunc‘𝐷) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝜑 → (𝐹:𝐵–1-1→𝐶 ∧ 𝐾:𝐶–onto→𝐵)) | ||
| Syntax | coppf 49681 | Extend class notation with the operation generating opposite functors. |
| class oppFunc | ||
| Definition | df-oppf 49682* | Definition of the operation generating opposite functors. Definition 3.41 of [Adamek] p. 39. The object part of the functor is unchanged while the morphism part is transposed due to reversed direction of arrows in the opposite category. The opposite functor is a functor on opposite categories (oppfoppc 49700). (Contributed by Zhi Wang, 4-Nov-2025.) Better reverse closure. (Revised by Zhi Wang, 13-Nov-2025.) |
| ⊢ oppFunc = (𝑓 ∈ V, 𝑔 ∈ V ↦ if((Rel 𝑔 ∧ Rel dom 𝑔), ⟨𝑓, tpos 𝑔⟩, ∅)) | ||
| Theorem | oppffn 49683 | oppFunc is a function on (V × V). (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ oppFunc Fn (V × V) | ||
| Theorem | reldmoppf 49684 | The domain of oppFunc is a relation. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ Rel dom oppFunc | ||
| Theorem | oppfvalg 49685 | Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 oppFunc 𝐺) = if((Rel 𝐺 ∧ Rel dom 𝐺), ⟨𝐹, tpos 𝐺⟩, ∅)) | ||
| Theorem | oppfrcllem 49686 | Lemma for oppfrcl 49687. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 ⇒ ⊢ (𝜑 → 𝐺 ≠ ∅) | ||
| Theorem | oppfrcl 49687 | 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 49688 | 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 49689 | 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 49690 | Rewrite the opposite functor into its components (eqopi 7991). (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ 𝑅) & ⊢ Rel 𝑅 & ⊢ 𝐺 = ( oppFunc ‘𝐹) & ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩) ⇒ ⊢ (𝜑 → (𝐺 ∈ (V × V) ∧ ((1st ‘𝐺) = 𝐴 ∧ (2nd ‘𝐺) = tpos 𝐵))) | ||
| Theorem | 2oppf 49691 | 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 49692 | 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 49693 | 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 49694 | Lemma for oppfval 49695. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (Rel 𝐺 ∧ Rel dom 𝐺)) | ||
| Theorem | oppfval 49695 | Value of the opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 oppFunc 𝐺) = ⟨𝐹, tpos 𝐺⟩) | ||
| Theorem | oppfval2 49696 | Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.) |
| ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → ( oppFunc ‘𝐹) = ⟨(1st ‘𝐹), tpos (2nd ‘𝐹)⟩) | ||
| Theorem | oppfval3 49697 | Value of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 = ⟨𝐺, 𝐾⟩) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( oppFunc ‘𝐹) = ⟨𝐺, tpos 𝐾⟩) | ||
| Theorem | oppf1 49698 | Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (1st ‘( oppFunc ‘𝐹)) = (1st ‘𝐹)) | ||
| Theorem | oppf2 49699 | Value of the morphism part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝑀(2nd ‘( oppFunc ‘𝐹))𝑁) = (𝑁(2nd ‘𝐹)𝑀)) | ||
| Theorem | oppfoppc 49700 | The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (𝐹 oppFunc 𝐺) ∈ (𝑂 Func 𝑃)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |