HomeTheorem List (p. 499 of 507)
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. 499 of 507) | < 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-31281) |
Hilbert Space Explorer
(31282-32804) |
Users' Mathboxes
(32805-50680) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mrelatlubALT 49801 | Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Zhi Wang, 29-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐼 = (toInc‘𝐶) & ⊢ 𝐹 = (mrCls‘𝐶) & ⊢ 𝐿 = (lub‘𝐼) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶) → (𝐿‘𝑈) = (𝐹‘∪ 𝑈)) | ||
| Theorem | mrelatglbALT 49802 | Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Zhi Wang, 29-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐼 = (toInc‘𝐶) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈) | ||
| Theorem | mreclat 49803 | A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
| Theorem | topclat 49804 | A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat) | ||
| Theorem | toplatglb0 49805 | The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽) | ||
| Theorem | toplatlub 49806 | Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑆 ⊆ 𝐽) & ⊢ 𝑈 = (lub‘𝐼) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆) | ||
| Theorem | toplatglb 49807 | Greatest lower bounds in a topology are realized by the interior of the intersection. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑆 ⊆ 𝐽) & ⊢ 𝐺 = (glb‘𝐼) & ⊢ (𝜑 → 𝑆 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = ((int‘𝐽)‘∩ 𝑆)) | ||
| Theorem | toplatjoin 49808 | Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∨ = (join‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵)) | ||
| Theorem | toplatmeet 49809 | Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∧ = (meet‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵)) | ||
| Theorem | topdlat 49810 | A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat) | ||
| Theorem | elmgpcntrd 49811* | The center of a ring. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntr‘𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑋)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑍) | ||
| Theorem | asclelbasALT 49812 | Alternate proof of asclelbas 22044. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊)) | ||
| Theorem | asclcntr 49813 | The algebra scalar lifting function maps into the center of the algebra. Equivalently, a lifted scalar is a center of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ 𝑀 = (mulGrp‘𝑊) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Cntr‘𝑀)) | ||
| Theorem | asclcom 49814 |
Scalars are commutative after being lifted.
However, the scalars themselves are not necessarily commutative if the algebra is not a faithful module. For example, Let 𝐹 be the 2 by 2 upper triangular matrix algebra over a commutative ring 𝑊. It is provable that 𝐹 is in general non-commutative. Define scalar multiplication 𝐶 · 𝑋 as multipying the top-left entry, which is a "vector" element of 𝑊, of the "scalar" 𝐶, which is now an upper triangular matrix, with the "vector" 𝑋 ∈ (Base‘𝑊). Equivalently, the algebra scalar lifting function is not necessarily injective unless the algebra is faithful. Therefore, all "scalar injection" was renamed. Alternate proof involves assa2ass 22024, assa2ass2 22025, and asclval 22040, by setting 𝑋 and 𝑌 the multiplicative identity of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ∗ = (.r‘𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶 ∗ 𝐷)) = (𝐴‘(𝐷 ∗ 𝐶))) | ||
| Theorem | homf0 49815 | The base is empty iff the functionalized Hom-set operation is empty. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ ((Base‘𝐶) = ∅ ↔ (Homf ‘𝐶) = ∅) | ||
| Theorem | catprslem 49816* | Lemma for catprs 49817. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
| Theorem | catprs 49817* | A preorder can be extracted from a category. See catprs2 49818 for more details. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | catprs2 49818* | A category equipped with the induced preorder, where an object 𝑥 is defined to be "less than or equal to" 𝑦 iff there is a morphism from 𝑥 to 𝑦, is a preordered set, or a proset. The category might not be thin. See catprsc 49819 and catprsc2 49820 for constructions satisfying the hypothesis "catprs.1". See catprs 49817 for a more primitive version. See prsthinc 50270 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
| Theorem | catprsc 49819* | A construction of the preorder induced by a category. See catprs2 49818 for details. See also catprsc2 49820 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | catprsc2 49820* | An alternate construction of the preorder induced by a category. See catprs2 49818 for details. See also catprsc 49819 for a different construction. The two constructions are different because df-cat 17730 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐻𝑦) ≠ ∅}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | endmndlem 49821 | A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 50384 for converting a monoid to a category. Lemma for bj-endmnd 37990. (Contributed by Zhi Wang, 25-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀)) & ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (+g‘𝑀)) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mnd) | ||
| Theorem | oppccatb 49822 | An opposite category is a category. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝑂 ∈ Cat)) | ||
| Theorem | oppcmndclem 49823 | Lemma for oppcmndc 49825. Everything is true for two distinct elements in a singleton or an empty set (since it is impossible). Note that if this theorem and oppcendc 49824 are in ¬ 𝑥 = 𝑦 form, then both proofs should be one step shorter. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = {𝐴}) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≠ 𝑌 → 𝜓)) | ||
| Theorem | oppcendc 49824* | The opposite category of a category whose morphisms are all endomorphisms has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅)) ⇒ ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂)) | ||
| Theorem | oppcmndc 49825 | The opposite category of a category whose base set is a singleton or an empty set has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐵 = {𝑋}) ⇒ ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂)) | ||
| Theorem | idmon 49826 | An identity arrow, or an identity morphism, is a monomorphism. (Contributed by Zhi Wang, 21-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑀 = (Mono‘𝐶) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝑀𝑋)) | ||
| Theorem | idepi 49827 | An identity arrow, or an identity morphism, is an epimorphism. (Contributed by Zhi Wang, 21-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐸 = (Epi‘𝐶) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐸𝑋)) | ||
| Theorem | sectrcl 49828 | Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | sectrcl2 49829 | Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | invrcl 49830 | Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | invrcl2 49831 | Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | isinv2 49832 | The property "𝐹 is an inverse of 𝐺". (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)) | ||
| Theorem | isisod 49833 | The predicate "is an isomorphism" (deduction form). (Contributed by Zhi Wang, 16-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑋)) & ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑋)𝐹) = ( 1 ‘𝑋)) & ⊢ (𝜑 → (𝐹(⟨𝑌, 𝑋⟩ · 𝑌)𝐺) = ( 1 ‘𝑌)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) | ||
| Theorem | upeu2lem 49834* | Lemma for upeu2 49978. There exists a unique morphism from 𝑌 to 𝑍 that commutes if 𝐹:𝑋⟶𝑌 is an isomorphism. (Contributed by Zhi Wang, 20-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑍)) ⇒ ⊢ (𝜑 → ∃!𝑘 ∈ (𝑌𝐻𝑍)𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)) | ||
| Theorem | sectfn 49835 | The function value of the function returning the sections of a category is a function over the Cartesian square of the base set of the category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → (Sect‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | invfn 49836 | The function value of the function returning the inverses of a category is a function over the Cartesian square of the base set of the category. Simplifies isofn 17838 (see isofnALT 49837). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → (Inv‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | isofnALT 49837 | The function value of the function returning the isomorphisms of a category is a function over the Cartesian square of the base set of the category. (Contributed by AV, 5-Apr-2020.) (Proof shortened by Zhi Wang, 3-Nov-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | isofval2 49838* | Function value of the function returning the isomorphisms of a category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ dom (𝑥𝑁𝑦))) | ||
| Theorem | isorcl 49839 | Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | isorcl2 49840 | Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | isoval2 49841 | The isomorphisms are the domain of the inverse relation. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌) | ||
| Theorem | sectpropdlem 49842 | Lemma for sectpropd 49843. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷)) | ||
| Theorem | sectpropd 49843 | Two structures with the same base, hom-sets and composition operation have the same sections. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (Sect‘𝐶) = (Sect‘𝐷)) | ||
| Theorem | invpropdlem 49844 | Lemma for invpropd 49845. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Inv‘𝐶)) → 𝑃 ∈ (Inv‘𝐷)) | ||
| Theorem | invpropd 49845 | Two structures with the same base, hom-sets and composition operation have the same inverses. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (Inv‘𝐶) = (Inv‘𝐷)) | ||
| Theorem | isopropdlem 49846 | Lemma for isopropd 49847. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Iso‘𝐶)) → 𝑃 ∈ (Iso‘𝐷)) | ||
| Theorem | isopropd 49847 | Two structures with the same base, hom-sets and composition operation have the same isomorphisms. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (Iso‘𝐶) = (Iso‘𝐷)) | ||
| Theorem | cicfn 49848 | ≃𝑐 is a function on Cat. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ ≃𝑐 Fn Cat | ||
| Theorem | cicrcl2 49849 | Isomorphism implies the structure being a category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 → 𝐶 ∈ Cat) | ||
| Theorem | oppccic 49850 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝐶)𝑆) ⇒ ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | relcic 49851 | The set of isomorphic objects is a relation. Simplifies cicer 17869 (see cicerALT 49852). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → Rel ( ≃𝑐 ‘𝐶)) | ||
| Theorem | cicerALT 49852 | 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 49853 | 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 49854 | Rewrite the predicate of isomorphic objects with separated parts. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝑃 ∈ ( ≃𝑐 ‘𝐶) → (1st ‘𝑃)( ≃𝑐 ‘𝐶)(2nd ‘𝑃)) | ||
| Theorem | cicpropdlem 49855 | Lemma for cicpropd 49856. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘𝐶)) → 𝑃 ∈ ( ≃𝑐 ‘𝐷)) | ||
| Theorem | cicpropd 49856 | 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 49857 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 ↔ 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | oppcciceq 49858 | The opposite category has the same isomorphic objects as the original category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ ( ≃𝑐 ‘𝐶) = ( ≃𝑐 ‘𝑂) | ||
| Theorem | dmdm 49859 | The double domain of a function on a Cartesian square. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ (𝐴 Fn (𝐵 × 𝐵) → 𝐵 = dom dom 𝐴) | ||
| Theorem | iinfssclem1 49860* | Lemma for iinfssc 49863. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 = (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝑆, 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 ↦ ∩ 𝑥 ∈ 𝐴 (𝑧𝐻𝑤))) | ||
| Theorem | iinfssclem2 49861* | Lemma for iinfssc 49863. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆)) | ||
| Theorem | iinfssclem3 49862* | Lemma for iinfssc 49863. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = ∩ 𝑥 ∈ 𝐴 (𝑋𝐻𝑌)) | ||
| Theorem | iinfssc 49863* | Indexed intersection of subcategories is a subcategory (the category-agnostic version). (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ⊆cat 𝐽) | ||
| Theorem | iinfsubc 49864* | Indexed intersection of subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶)) | ||
| Theorem | iinfprg 49865* | Indexed intersection of functions with an unordered pair index. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) = (𝑥 ∈ ∩ 𝑦 ∈ {𝐴, 𝐵}dom 𝑦 ↦ ∩ 𝑦 ∈ {𝐴, 𝐵} (𝑦‘𝑥))) | ||
| Theorem | infsubc 49866* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ (Subcat‘𝐶) ∧ 𝐵 ∈ (Subcat‘𝐶)) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) ∈ (Subcat‘𝐶)) | ||
| Theorem | infsubc2 49867* | 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 49868* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑇), 𝑦 ∈ (𝑆 ∩ 𝑇) ↦ ((𝑥𝐻𝑦) ∩ (𝑥𝐽𝑦))) ∈ (Subcat‘𝐶)) | ||
| Theorem | discsubclem 49869* | Lemma for discsubc 49870. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) ⇒ ⊢ 𝐽 Fn (𝑆 × 𝑆) | ||
| Theorem | discsubc 49870* | 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 49871* | Lemma for iinfconstbas 49872. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 = ((Subcat‘𝐶) ∩ {𝑗 ∣ 𝑗 Fn (𝑆 × 𝑆)})) ⇒ ⊢ (𝜑 → 𝐽 ∈ 𝐴) | ||
| Theorem | iinfconstbas 49872* | 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 49873* | Lemma for nelsubc 49874. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ 𝐻 = (Homf ‘𝐶) ⇒ ⊢ (𝜑 → (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat 𝐻 ∧ (¬ ∀𝑥 ∈ 𝑆 𝐼 ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)𝜓)))) | ||
| Theorem | nelsubc 49874* | 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 49875 | An empty "hom-set" for non-empty base is not a subcategory. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → ¬ 𝐽 ∈ (Subcat‘𝐶)) | ||
| Theorem | nelsubc3lem 49876* | Lemma for nelsubc3 49877. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 ∈ Cat & ⊢ 𝐽 ∈ V & ⊢ 𝑆 ∈ V & ⊢ (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))) ⇒ ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) | ||
| Theorem | nelsubc3 49877* |
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 17875 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 17912). To construct such a category, see setc1onsubc 50408 and cnelsubc 50410. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) | ||
| Theorem | ssccatid 49878* | 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 50410). (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐽 ⊆cat 𝐻) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 1 ∈ (𝑦𝐽𝑦)) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ (𝑎𝐽𝑏))) → ( 1 (⟨𝑎, 𝑏⟩ · 𝑏)𝑚) = 𝑚) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ (𝑎𝐽𝑏))) → (𝑚(⟨𝑎, 𝑎⟩ · 𝑏) 1 ) = 𝑚) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐽𝑧)) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑦 ∈ 𝑆 ↦ 1 ))) | ||
| Theorem | resccatlem 49879* | Lemma for resccat 49880. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑆 = (Base‘𝐸) & ⊢ 𝐽 = (Homf ‘𝐸) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐸) & ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ↔ 𝐸 ∈ Cat)) | ||
| Theorem | resccat 49880* | 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 49881 | The domain of Func is a relation. (Contributed by Zhi Wang, 12-Nov-2025.) |
| ⊢ Rel dom Func | ||
| Theorem | func1st2nd 49882 | Rewrite the functor predicate with separated parts. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | ||
| Theorem | func1st 49883 | Extract the first member of a functor. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹) | ||
| Theorem | func2nd 49884 | Extract the second member of a functor. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺) | ||
| Theorem | funcrcl2 49885 | Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
| Theorem | funcrcl3 49886 | Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐸 ∈ Cat) | ||
| Theorem | funcf2lem 49887* | 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 49888* | A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = (𝐸‘𝐶) ⇒ ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | 0funcglem 49889 | Lemma for 0funcg 49891. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ (𝜑 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → (𝜃 ↔ 𝜁)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜂 ∧ 𝜁))) | ||
| Theorem | 0funcg2 49890 | The functor from the empty category. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ∅ = (Base‘𝐶)) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ (𝐹 = ∅ ∧ 𝐺 = ∅))) | ||
| Theorem | 0funcg 49891 | 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 49892 | Lemma for 0funcALT 49894. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ (𝜒 ↔ 𝜂) & ⊢ (𝜃 ↔ 𝜁) & ⊢ 𝜏 ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜂 ∧ 𝜁))) | ||
| Theorem | 0func 49893 | 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 49894 | Alternate proof of 0func 49893. (Contributed by Zhi Wang, 7-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (∅ Func 𝐶) = {⟨∅, ∅⟩}) | ||
| Theorem | func0g 49895 | 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 49896 | 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 49897* | 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 49898 | 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 49899 | 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 49900 | Value of the object part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿) & ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = (𝑀‘𝑋)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |