HomeTheorem List (p. 497 of 505)
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 505) | < 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-31123) |
Hilbert Space Explorer
(31124-32646) |
Users' Mathboxes
(32647-50431) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | resipos 49601 | A set equipped with an order where no distinct elements are comparable is a poset. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐾 ∈ Poset) | ||
| Theorem | exbaspos 49602* | There exists a poset for any base set. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Poset 𝐵 = (Base‘𝑘)) | ||
| Theorem | exbasprs 49603* | There exists a preordered set for any base set. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Proset 𝐵 = (Base‘𝑘)) | ||
| Theorem | basresposfo 49604 | The base function restricted to the class of posets maps the class of posets onto the universal class. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (Base ↾ Poset):Poset–onto→V | ||
| Theorem | basresprsfo 49605 | The base function restricted to the class of preordered sets maps the class of preordered sets onto the universal class. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (Base ↾ Proset ): Proset –onto→V | ||
| Theorem | posnex 49606 | The class of posets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ Poset ∉ V | ||
| Theorem | prsnex 49607 | The class of preordered sets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ Proset ∉ V | ||
| Theorem | toslat 49608 | A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024.) |
| ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Lat) | ||
| Theorem | isclatd 49609* | The predicate "is a complete lattice" (deduction form). (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝑈 = (lub‘𝐾)) & ⊢ (𝜑 → 𝐺 = (glb‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝑈) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝐺) ⇒ ⊢ (𝜑 → 𝐾 ∈ CLat) | ||
| Theorem | intubeu 49610* | Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ (𝐶 ∈ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ ∀𝑦 ∈ 𝐵 (𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦)) ↔ 𝐶 = ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥})) | ||
| Theorem | unilbeu 49611* | Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴})) | ||
| Theorem | ipolublem 49612* | Lemma for ipolubdm 49613 and ipolub 49614. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧)))) | ||
| Theorem | ipolubdm 49613* | The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹)) | ||
| Theorem | ipolub 49614* | The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18446 is in quantified form. mrelatlub 18596 could potentially be shortened using this. See mrelatlubALT 49621. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
| Theorem | ipoglblem 49615* | Lemma for ipoglbdm 49616 and ipoglb 49617. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋)))) | ||
| Theorem | ipoglbdm 49616* | The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹)) | ||
| Theorem | ipoglb 49617* | The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18447 is in quantified form. mrelatglb 18594 could potentially be shortened using this. See mrelatglbALT 49622. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇) | ||
| Theorem | ipolub0 49618 | The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹) | ||
| Theorem | ipolub00 49619 | 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 49620 | The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹) | ||
| Theorem | mrelatlubALT 49621 | 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 49622 | 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 49623 | A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
| Theorem | topclat 49624 | A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat) | ||
| Theorem | toplatglb0 49625 | The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽) | ||
| Theorem | toplatlub 49626 | Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑆 ⊆ 𝐽) & ⊢ 𝑈 = (lub‘𝐼) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆) | ||
| Theorem | toplatglb 49627 | 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 49628 | Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∨ = (join‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵)) | ||
| Theorem | toplatmeet 49629 | Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∧ = (meet‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵)) | ||
| Theorem | topdlat 49630 | A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat) | ||
| Theorem | elmgpcntrd 49631* | The center of a ring. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntr‘𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑋)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑍) | ||
| Theorem | asclelbasALT 49632 | Alternate proof of asclelbas 21937. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊)) | ||
| Theorem | asclcntr 49633 | 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 49634 |
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 21917, assa2ass2 21918, and asclval 21933, by setting 𝑋 and 𝑌 the multiplicative identity of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ∗ = (.r‘𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶 ∗ 𝐷)) = (𝐴‘(𝐷 ∗ 𝐶))) | ||
| Theorem | homf0 49635 | The base is empty iff the functionalized Hom-set operation is empty. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ ((Base‘𝐶) = ∅ ↔ (Homf ‘𝐶) = ∅) | ||
| Theorem | catprslem 49636* | Lemma for catprs 49637. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
| Theorem | catprs 49637* | A preorder can be extracted from a category. See catprs2 49638 for more details. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | catprs2 49638* | 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 49639 and catprsc2 49640 for constructions satisfying the hypothesis "catprs.1". See catprs 49637 for a more primitive version. See prsthinc 50090 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
| Theorem | catprsc 49639* | A construction of the preorder induced by a category. See catprs2 49638 for details. See also catprsc2 49640 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | catprsc2 49640* | An alternate construction of the preorder induced by a category. See catprs2 49638 for details. See also catprsc 49639 for a different construction. The two constructions are different because df-cat 17702 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐻𝑦) ≠ ∅}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | endmndlem 49641 | A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 50204 for converting a monoid to a category. Lemma for bj-endmnd 37815. (Contributed by Zhi Wang, 25-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀)) & ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (+g‘𝑀)) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mnd) | ||
| Theorem | oppccatb 49642 | An opposite category is a category. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝑂 ∈ Cat)) | ||
| Theorem | oppcmndclem 49643 | Lemma for oppcmndc 49645. 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 49644 are in ¬ 𝑥 = 𝑦 form, then both proofs should be one step shorter. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = {𝐴}) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≠ 𝑌 → 𝜓)) | ||
| Theorem | oppcendc 49644* | 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 49645 | 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 49646 | 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 49647 | 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 49648 | Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | sectrcl2 49649 | Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | invrcl 49650 | Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | invrcl2 49651 | Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | isinv2 49652 | The property "𝐹 is an inverse of 𝐺". (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)) | ||
| Theorem | isisod 49653 | 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 49654* | Lemma for upeu2 49798. 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 49655 | 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 49656 | 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 17810 (see isofnALT 49657). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → (Inv‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | isofnALT 49657 | 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 49658* | 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 49659 | Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | isorcl2 49660 | Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | isoval2 49661 | The isomorphisms are the domain of the inverse relation. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌) | ||
| Theorem | sectpropdlem 49662 | Lemma for sectpropd 49663. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷)) | ||
| Theorem | sectpropd 49663 | 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 49664 | Lemma for invpropd 49665. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Inv‘𝐶)) → 𝑃 ∈ (Inv‘𝐷)) | ||
| Theorem | invpropd 49665 | 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 49666 | Lemma for isopropd 49667. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Iso‘𝐶)) → 𝑃 ∈ (Iso‘𝐷)) | ||
| Theorem | isopropd 49667 | 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 49668 | ≃𝑐 is a function on Cat. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ ≃𝑐 Fn Cat | ||
| Theorem | cicrcl2 49669 | Isomorphism implies the structure being a category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 → 𝐶 ∈ Cat) | ||
| Theorem | oppccic 49670 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝐶)𝑆) ⇒ ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | relcic 49671 | The set of isomorphic objects is a relation. Simplifies cicer 17841 (see cicerALT 49672). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → Rel ( ≃𝑐 ‘𝐶)) | ||
| Theorem | cicerALT 49672 | 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 49673 | 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 49674 | Rewrite the predicate of isomorphic objects with separated parts. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝑃 ∈ ( ≃𝑐 ‘𝐶) → (1st ‘𝑃)( ≃𝑐 ‘𝐶)(2nd ‘𝑃)) | ||
| Theorem | cicpropdlem 49675 | Lemma for cicpropd 49676. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘𝐶)) → 𝑃 ∈ ( ≃𝑐 ‘𝐷)) | ||
| Theorem | cicpropd 49676 | 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 49677 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 ↔ 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | oppcciceq 49678 | The opposite category has the same isomorphic objects as the original category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ ( ≃𝑐 ‘𝐶) = ( ≃𝑐 ‘𝑂) | ||
| Theorem | dmdm 49679 | The double domain of a function on a Cartesian square. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ (𝐴 Fn (𝐵 × 𝐵) → 𝐵 = dom dom 𝐴) | ||
| Theorem | iinfssclem1 49680* | Lemma for iinfssc 49683. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 = (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝑆, 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 ↦ ∩ 𝑥 ∈ 𝐴 (𝑧𝐻𝑤))) | ||
| Theorem | iinfssclem2 49681* | Lemma for iinfssc 49683. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆)) | ||
| Theorem | iinfssclem3 49682* | Lemma for iinfssc 49683. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = ∩ 𝑥 ∈ 𝐴 (𝑋𝐻𝑌)) | ||
| Theorem | iinfssc 49683* | Indexed intersection of subcategories is a subcategory (the category-agnostic version). (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ⊆cat 𝐽) | ||
| Theorem | iinfsubc 49684* | Indexed intersection of subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶)) | ||
| Theorem | iinfprg 49685* | Indexed intersection of functions with an unordered pair index. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) = (𝑥 ∈ ∩ 𝑦 ∈ {𝐴, 𝐵}dom 𝑦 ↦ ∩ 𝑦 ∈ {𝐴, 𝐵} (𝑦‘𝑥))) | ||
| Theorem | infsubc 49686* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ (Subcat‘𝐶) ∧ 𝐵 ∈ (Subcat‘𝐶)) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) ∈ (Subcat‘𝐶)) | ||
| Theorem | infsubc2 49687* | 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 49688* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑇), 𝑦 ∈ (𝑆 ∩ 𝑇) ↦ ((𝑥𝐻𝑦) ∩ (𝑥𝐽𝑦))) ∈ (Subcat‘𝐶)) | ||
| Theorem | discsubclem 49689* | Lemma for discsubc 49690. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) ⇒ ⊢ 𝐽 Fn (𝑆 × 𝑆) | ||
| Theorem | discsubc 49690* | 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 49691* | Lemma for iinfconstbas 49692. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 = ((Subcat‘𝐶) ∩ {𝑗 ∣ 𝑗 Fn (𝑆 × 𝑆)})) ⇒ ⊢ (𝜑 → 𝐽 ∈ 𝐴) | ||
| Theorem | iinfconstbas 49692* | 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 49693* | Lemma for nelsubc 49694. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ 𝐻 = (Homf ‘𝐶) ⇒ ⊢ (𝜑 → (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat 𝐻 ∧ (¬ ∀𝑥 ∈ 𝑆 𝐼 ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)𝜓)))) | ||
| Theorem | nelsubc 49694* | 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 49695 | An empty "hom-set" for non-empty base is not a subcategory. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ (𝜑 → 𝐽 = ((𝑆 × 𝑆) × {∅})) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → ¬ 𝐽 ∈ (Subcat‘𝐶)) | ||
| Theorem | nelsubc3lem 49696* | Lemma for nelsubc3 49697. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ 𝐶 ∈ Cat & ⊢ 𝐽 ∈ V & ⊢ 𝑆 ∈ V & ⊢ (𝐽 Fn (𝑆 × 𝑆) ∧ (𝐽 ⊆cat (Homf ‘𝐶) ∧ (¬ ∀𝑥 ∈ 𝑆 ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)))) ⇒ ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) | ||
| Theorem | nelsubc3 49697* |
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 17847 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 17884). To construct such a category, see setc1onsubc 50228 and cnelsubc 50230. (Contributed by Zhi Wang, 5-Nov-2025.) |
| ⊢ ∃𝑐 ∈ Cat ∃𝑗∃𝑠(𝑗 Fn (𝑠 × 𝑠) ∧ (𝑗 ⊆cat (Homf ‘𝑐) ∧ (¬ ∀𝑥 ∈ 𝑠 ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))) | ||
| Theorem | ssccatid 49698* | 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 50230). (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐽 ⊆cat 𝐻) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 1 ∈ (𝑦𝐽𝑦)) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ (𝑎𝐽𝑏))) → ( 1 (⟨𝑎, 𝑏⟩ · 𝑏)𝑚) = 𝑚) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ (𝑎𝐽𝑏))) → (𝑚(⟨𝑎, 𝑎⟩ · 𝑏) 1 ) = 𝑚) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐽𝑧)) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑦 ∈ 𝑆 ↦ 1 ))) | ||
| Theorem | resccatlem 49699* | Lemma for resccat 49700. (Contributed by Zhi Wang, 6-Nov-2025.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑆 = (Base‘𝐸) & ⊢ 𝐽 = (Homf ‘𝐸) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐸) & ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ↔ 𝐸 ∈ Cat)) | ||
| Theorem | resccat 49700* | 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)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |