HomeTheorem List (p. 490 of 497)
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. 490 of 497) | < 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-30854) |
Hilbert Space Explorer
(30855-32377) |
Users' Mathboxes
(32378-49671) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | unilbeu 48901* | Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴})) | ||
| Theorem | ipolublem 48902* | Lemma for ipolubdm 48903 and ipolub 48904. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧)))) | ||
| Theorem | ipolubdm 48903* | The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹)) | ||
| Theorem | ipolub 48904* | The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18379 is in quantified form. mrelatlub 18527 could potentially be shortened using this. See mrelatlubALT 48911. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
| Theorem | ipoglblem 48905* | Lemma for ipoglbdm 48906 and ipoglb 48907. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋)))) | ||
| Theorem | ipoglbdm 48906* | The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹)) | ||
| Theorem | ipoglb 48907* | The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18380 is in quantified form. mrelatglb 18525 could potentially be shortened using this. See mrelatglbALT 48912. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇) | ||
| Theorem | ipolub0 48908 | The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹) | ||
| Theorem | ipolub00 48909 | The LUB of the empty set is the empty set if it is contained. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → ∅ ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑈‘∅) = ∅) | ||
| Theorem | ipoglb0 48910 | The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹) | ||
| Theorem | mrelatlubALT 48911 | 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 48912 | 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 48913 | A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
| Theorem | topclat 48914 | A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat) | ||
| Theorem | toplatglb0 48915 | The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽) | ||
| Theorem | toplatlub 48916 | Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑆 ⊆ 𝐽) & ⊢ 𝑈 = (lub‘𝐼) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆) | ||
| Theorem | toplatglb 48917 | 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 48918 | Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∨ = (join‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵)) | ||
| Theorem | toplatmeet 48919 | Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∧ = (meet‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵)) | ||
| Theorem | topdlat 48920 | A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat) | ||
| Theorem | elmgpcntrd 48921* | The center of a ring. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntr‘𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑋)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑍) | ||
| Theorem | asclelbas 48922 | Lifted scalars are in the base set of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof shortened by Thierry Arnoux, 22-Sep-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊)) | ||
| Theorem | asclelbasALT 48923 | Alternate proof of asclelbas 48922. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊)) | ||
| Theorem | asclcntr 48924 | 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 48925 |
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 21778, assa2ass2 21779, and asclval 21795, by setting 𝑋 and 𝑌 the multiplicative identity of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ∗ = (.r‘𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶 ∗ 𝐷)) = (𝐴‘(𝐷 ∗ 𝐶))) | ||
| Theorem | homf0 48926 | The base is empty iff the functionalized Hom-set operation is empty. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ ((Base‘𝐶) = ∅ ↔ (Homf ‘𝐶) = ∅) | ||
| Theorem | catprslem 48927* | Lemma for catprs 48928. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
| Theorem | catprs 48928* | A preorder can be extracted from a category. See catprs2 48929 for more details. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | catprs2 48929* | 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 48930 and catprsc2 48931 for constructions satisfying the hypothesis "catprs.1". See catprs 48928 for a more primitive version. See prsthinc 49342 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
| Theorem | catprsc 48930* | A construction of the preorder induced by a category. See catprs2 48929 for details. See also catprsc2 48931 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | catprsc2 48931* | An alternate construction of the preorder induced by a category. See catprs2 48929 for details. See also catprsc 48930 for a different construction. The two constructions are different because df-cat 17635 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐻𝑦) ≠ ∅}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | endmndlem 48932 | A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 49456 for converting a monoid to a category. Lemma for bj-endmnd 37303. (Contributed by Zhi Wang, 25-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀)) & ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (+g‘𝑀)) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mnd) | ||
| Theorem | oppccatb 48933 | An opposite category is a category. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝑂 ∈ Cat)) | ||
| Theorem | oppcmndclem 48934 | Lemma for oppcmndc 48936. 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 48935 are in ¬ 𝑥 = 𝑦 form, then both proofs should be one step shorter. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = {𝐴}) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≠ 𝑌 → 𝜓)) | ||
| Theorem | oppcendc 48935* | 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 48936 | 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 48937 | 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 48938 | 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 48939 | Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | sectrcl2 48940 | Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | invrcl 48941 | Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | invrcl2 48942 | Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | isinv2 48943 | The property "𝐹 is an inverse of 𝐺". (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)) | ||
| Theorem | isisod 48944 | 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 48945* | Lemma for upeu2 49080. 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 48946 | 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 48947 | 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 17743 (see isofnALT 48948). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → (Inv‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | isofnALT 48948 | 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 48949* | 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 48950 | Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | isorcl2 48951 | Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | isoval2 48952 | The isomorphisms are the domain of the inverse relation. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌) | ||
| Theorem | sectpropdlem 48953 | Lemma for sectpropd 48954. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷)) | ||
| Theorem | sectpropd 48954 | 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 48955 | Lemma for invpropd 48956. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Inv‘𝐶)) → 𝑃 ∈ (Inv‘𝐷)) | ||
| Theorem | invpropd 48956 | 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 48957 | Lemma for isopropd 48958. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Iso‘𝐶)) → 𝑃 ∈ (Iso‘𝐷)) | ||
| Theorem | isopropd 48958 | 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 48959 | ≃𝑐 is a function on Cat. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ ≃𝑐 Fn Cat | ||
| Theorem | cicrcl2 48960 | Isomorphism implies the structure being a category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 → 𝐶 ∈ Cat) | ||
| Theorem | oppccic 48961 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝐶)𝑆) ⇒ ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | relcic 48962 | The set of isomorphic objects is a relation. Simplifies cicer 17774 (see cicerALT 48963). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → Rel ( ≃𝑐 ‘𝐶)) | ||
| Theorem | cicerALT 48963 | 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 48964 | 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 48965 | Rewrite the predicate of isomorphic objects with separated parts. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝑃 ∈ ( ≃𝑐 ‘𝐶) → (1st ‘𝑃)( ≃𝑐 ‘𝐶)(2nd ‘𝑃)) | ||
| Theorem | cicpropdlem 48966 | Lemma for cicpropd 48967. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘𝐶)) → 𝑃 ∈ ( ≃𝑐 ‘𝐷)) | ||
| Theorem | cicpropd 48967 | 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 48968 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 ↔ 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | oppcciceq 48969 | The opposite category has the same isomorphic objects as the original category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ ( ≃𝑐 ‘𝐶) = ( ≃𝑐 ‘𝑂) | ||
| Theorem | dmdm 48970 | The double domain of a function on a Cartesian square. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ (𝐴 Fn (𝐵 × 𝐵) → 𝐵 = dom dom 𝐴) | ||
| Theorem | iinfssclem1 48971* | Lemma for iinfssc 48974. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 = (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝑆, 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 ↦ ∩ 𝑥 ∈ 𝐴 (𝑧𝐻𝑤))) | ||
| Theorem | iinfssclem2 48972* | Lemma for iinfssc 48974. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆)) | ||
| Theorem | iinfssclem3 48973* | Lemma for iinfssc 48974. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = ∩ 𝑥 ∈ 𝐴 (𝑋𝐻𝑌)) | ||
| Theorem | iinfssc 48974* | Indexed intersection of subcategories is a subcategory (the category-agnostic version). (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ⊆cat 𝐽) | ||
| Theorem | iinfsubc 48975* | Indexed intersection of subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶)) | ||
| Theorem | iinfprg 48976* | Indexed intersection of functions with an unordered pair index. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) = (𝑥 ∈ ∩ 𝑦 ∈ {𝐴, 𝐵}dom 𝑦 ↦ ∩ 𝑦 ∈ {𝐴, 𝐵} (𝑦‘𝑥))) | ||
| Theorem | infsubc 48977* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ (Subcat‘𝐶) ∧ 𝐵 ∈ (Subcat‘𝐶)) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) ∈ (Subcat‘𝐶)) | ||
| Theorem | infsubc2 48978* | 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 48979* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑇), 𝑦 ∈ (𝑆 ∩ 𝑇) ↦ ((𝑥𝐻𝑦) ∩ (𝑥𝐽𝑦))) ∈ (Subcat‘𝐶)) | ||
| Theorem | discsubclem 48980* | Lemma for discsubc 48981. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) ⇒ ⊢ 𝐽 Fn (𝑆 × 𝑆) | ||
| Theorem | discsubc 48981* | 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 48982* | Lemma for iinfconstbas 48983. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 = ((Subcat‘𝐶) ∩ {𝑗 ∣ 𝑗 Fn (𝑆 × 𝑆)})) ⇒ ⊢ (𝜑 → 𝐽 ∈ 𝐴) | ||
| Theorem | iinfconstbas 48983* | 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 48984* | Lemma for nelsubc 48985. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ 𝐻 = (Homf ‘𝐶) ⇒ ⊢ (𝜑 → (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat 𝐻 ∧ (¬ ∀𝑥 ∈ 𝑆 𝐼 ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)𝜓)))) | ||
| Theorem | nelsubc 48985* | 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 48986 | An empty "hom-set" for non-empty base is not a subcategory. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → ¬ 𝐽 ∈ (Subcat‘𝐶)) | ||
| Theorem | nelsubc3lem 48987* | Lemma for nelsubc3 48988. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 ∈ Cat & ⊢ 𝐽 ∈ V & ⊢ 𝑆 ∈ V & ⊢ (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))) ⇒ ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) | ||
| Theorem | nelsubc3 48988* |
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 17780 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 17817). To construct such a category, see setc1onsubc 49480 and cnelsubc 49482. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) | ||
| Theorem | ssccatid 48989* | 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 49482). (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐽 ⊆cat 𝐻) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 1 ∈ (𝑦𝐽𝑦)) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ (𝑎𝐽𝑏))) → ( 1 (⟨𝑎, 𝑏⟩ · 𝑏)𝑚) = 𝑚) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ (𝑎𝐽𝑏))) → (𝑚(⟨𝑎, 𝑎⟩ · 𝑏) 1 ) = 𝑚) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐽𝑧)) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑦 ∈ 𝑆 ↦ 1 ))) | ||
| Theorem | resccatlem 48990* | Lemma for resccat 48991. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑆 = (Base‘𝐸) & ⊢ 𝐽 = (Homf ‘𝐸) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐸) & ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ↔ 𝐸 ∈ Cat)) | ||
| Theorem | resccat 48991* | 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 48992 | The domain of Func is a relation. (Contributed by Zhi Wang, 12-Nov-2025.) |
| ⊢ Rel dom Func | ||
| Theorem | func1st2nd 48993 | Rewrite the functor predicate with separated parts. (Contributed by Zhi Wang, 19-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | ||
| Theorem | func1st 48994 | Extract the first member of a functor. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹) | ||
| Theorem | func2nd 48995 | Extract the second member of a functor. (Contributed by Zhi Wang, 15-Nov-2025.) |
| ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺) | ||
| Theorem | funcrcl2 48996 | Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
| Theorem | funcrcl3 48997 | Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐸 ∈ Cat) | ||
| Theorem | funcf2lem 48998* | 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 48999* | A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = (𝐸‘𝐶) ⇒ ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | 0funcglem 49000 | Lemma for 0funcg 49002. (Contributed by Zhi Wang, 17-Oct-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ (𝜑 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → (𝜃 ↔ 𝜁)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜂 ∧ 𝜁))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |