![]() |
Metamath
Proof Explorer Theorem List (p. 478 of 480) | < 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: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ipolub 47701* | The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18372 is in quantified form. mrelatlub 18520 could potentially be shortened using this. See mrelatlubALT 47708. (Contributed by Zhi Wang, 28-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
Theorem | ipoglblem 47702* | Lemma for ipoglbdm 47703 and ipoglb 47704. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋)))) | ||
Theorem | ipoglbdm 47703* | The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹)) | ||
Theorem | ipoglb 47704* | The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18373 is in quantified form. mrelatglb 18518 could potentially be shortened using this. See mrelatglbALT 47709. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇) | ||
Theorem | ipolub0 47705 | The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹) | ||
Theorem | ipolub00 47706 | 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 47707 | The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹) | ||
Theorem | mrelatlubALT 47708 | 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 47709 | 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 47710 | A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
Theorem | topclat 47711 | A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat) | ||
Theorem | toplatglb0 47712 | The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽) | ||
Theorem | toplatlub 47713 | Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑆 ⊆ 𝐽) & ⊢ 𝑈 = (lub‘𝐼) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆) | ||
Theorem | toplatglb 47714 | 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 47715 | Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∨ = (join‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵)) | ||
Theorem | toplatmeet 47716 | Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∧ = (meet‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵)) | ||
Theorem | topdlat 47717 | A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat) | ||
Theorem | catprslem 47718* | Lemma for catprs 47719. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
Theorem | catprs 47719* | A preorder can be extracted from a category. See catprs2 47720 for more details. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
Theorem | catprs2 47720* | 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 47721 and catprsc2 47722 for constructions satisfying the hypothesis "catprs.1". See catprs 47719 for a more primitive version. See prsthinc 47762 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
Theorem | catprsc 47721* | A construction of the preorder induced by a category. See catprs2 47720 for details. See also catprsc2 47722 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → ≤ = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
Theorem | catprsc2 47722* | An alternate construction of the preorder induced by a category. See catprs2 47720 for details. See also catprsc 47721 for a different construction. The two constructions are different because df-cat 17617 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (𝜑 → ≤ = {〈𝑥, 𝑦〉 ∣ (𝑥𝐻𝑦) ≠ ∅}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
Theorem | endmndlem 47723 | A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 47792 for converting a monoid to a category. Lemma for bj-endmnd 36503. (Contributed by Zhi Wang, 25-Sep-2024.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀)) & ⊢ (𝜑 → (〈𝑋, 𝑋〉 · 𝑋) = (+g‘𝑀)) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mnd) | ||
Theorem | idmon 47724 | 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 47725 | 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 | funcf2lem 47726* | A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
Syntax | cthinc 47727 | Extend class notation with the class of thin categories. |
class ThinCat | ||
Definition | df-thinc 47728* | Definition of the class of thin categories, or posetal categories, whose hom-sets each contain at most one morphism. Example 3.26(2) of [Adamek] p. 33. "ThinCat" was taken instead of "PosCat" because the latter might mean the category of posets. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ ThinCat = {𝑐 ∈ Cat ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)} | ||
Theorem | isthinc 47729* | The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))) | ||
Theorem | isthinc2 47730* | A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ≼ 1o)) | ||
Theorem | isthinc3 47731* | A thin category is a category in which, given a pair of objects 𝑥 and 𝑦 and any two morphisms 𝑓, 𝑔 from 𝑥 to 𝑦, the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑥𝐻𝑦)𝑓 = 𝑔)) | ||
Theorem | thincc 47732 | A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝐶 ∈ ThinCat → 𝐶 ∈ Cat) | ||
Theorem | thinccd 47733 | A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
Theorem | thincssc 47734 | A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ ThinCat ⊆ Cat | ||
Theorem | isthincd2lem1 47735* | Lemma for isthincd2 47746 and thincmo2 47736. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | thincmo2 47736 | Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | thincmo 47737* | There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
Theorem | thincmoALT 47738* | Alternate proof for thincmo 47737. (Contributed by Zhi Wang, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
Theorem | thincmod 47739* | At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
Theorem | thincn0eu 47740* | In a thin category, a hom-set being non-empty is equivalent to having a unique element. (Contributed by Zhi Wang, 21-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → ((𝑋𝐻𝑌) ≠ ∅ ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌))) | ||
Theorem | thincid 47741 | In a thin category, a morphism from an object to itself is an identity morphism. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑋)) ⇒ ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑋)) | ||
Theorem | thincmon 47742 | In a thin category, all morphisms are monomorphisms. The converse does not hold. See grptcmon 47804. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑀 = (Mono‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌)) | ||
Theorem | thincepi 47743 | In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi 47805. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐸 = (Epi‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌)) | ||
Theorem | isthincd2lem2 47744* | Lemma for isthincd2 47746. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)) | ||
Theorem | isthincd 47745* | The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
Theorem | isthincd2 47746* | The predicate "𝐶 is a thin category" without knowing 𝐶 is a category (deduction form). The identity arrow operator is also provided as a byproduct. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)))) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦)) & ⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) | ||
Theorem | oppcthin 47747 | The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat) | ||
Theorem | subthinc 47748 | A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐷 ∈ ThinCat) | ||
Theorem | functhinclem1 47749* | Lemma for functhinc 47753. Given the object part, there is only one possible morphism part such that the mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ ThinCat) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) & ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅)) ⇒ ⊢ (𝜑 → ((𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝐺𝑤):(𝑧𝐻𝑤)⟶((𝐹‘𝑧)𝐽(𝐹‘𝑤))) ↔ 𝐺 = 𝐾)) | ||
Theorem | functhinclem2 47750* | Lemma for functhinc 47753. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅)) ⇒ ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅)) | ||
Theorem | functhinclem3 47751* | Lemma for functhinc 47753. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))) & ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅)) & ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
Theorem | functhinclem4 47752* | Lemma for functhinc 47753. Other requirements on the morphism part are automatically satisfied. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ ThinCat) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅)) & ⊢ 1 = (Id‘𝐷) & ⊢ 𝐼 = (Id‘𝐸) & ⊢ · = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝐸) ⇒ ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(〈𝑎, 𝑏〉 · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(〈(𝐹‘𝑎), (𝐹‘𝑏)〉𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚)))) | ||
Theorem | functhinc 47753* | A functor to a thin category is determined entirely by the object part. The hypothesis "functhinc.1" is related to a monotone function if preorders induced by the categories are considered (catprs2 47720). (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ ThinCat) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅)) ⇒ ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾)) | ||
Theorem | fullthinc 47754* | A functor to a thin category is full iff empty hom-sets are mapped to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ ThinCat) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥𝐻𝑦) = ∅ → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅))) | ||
Theorem | fullthinc2 47755 | A full functor to a thin category maps empty hom-sets to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ ThinCat) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋𝐻𝑌) = ∅ ↔ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅)) | ||
Theorem | thincfth 47756 | A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) | ||
Theorem | thincciso 47757* | Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of [Adamek] p. 33. (Contributed by Zhi Wang, 16-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑅 = (Base‘𝑋) & ⊢ 𝑆 = (Base‘𝑌) & ⊢ 𝐻 = (Hom ‘𝑋) & ⊢ 𝐽 = (Hom ‘𝑌) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ThinCat) & ⊢ (𝜑 → 𝑌 ∈ ThinCat) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆))) | ||
Theorem | 0thincg 47758 | Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat) | ||
Theorem | 0thinc 47759 | The empty category (see 0cat 17638) is thin. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ ∅ ∈ ThinCat | ||
Theorem | indthinc 47760* | An indiscrete category in which all hom-sets have exactly one morphism is a thin category. Constructed here is an indiscrete category where all morphisms are ∅. This is a special case of prsthinc 47762, where ≤ = (𝐵 × 𝐵). This theorem also implies a functor from the category of sets to the category of small categories. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof shortened by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶)) & ⊢ (𝜑 → ∅ = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) | ||
Theorem | indthincALT 47761* | An alternate proof for indthinc 47760 assuming more axioms including ax-pow 5363 and ax-un 7729. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶)) & ⊢ (𝜑 → ∅ = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) | ||
Theorem | prsthinc 47762* | Preordered sets as categories. Similar to example 3.3(4.d) of [Adamek] p. 24, but the hom-sets are not pairwise disjoint. One can define a functor from the category of prosets to the category of small thin categories. See catprs 47719 and catprs2 47720 for inducing a preorder from a category. Example 3.26(2) of [Adamek] p. 33 indicates that it induces a bijection from the equivalence class of isomorphic small thin categories to the equivalence class of order-isomorphic preordered sets. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶)) & ⊢ (𝜑 → ∅ = (comp‘𝐶)) & ⊢ (𝜑 → ≤ = (le‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) | ||
Theorem | setcthin 47763* | A category of sets all of whose objects contain at most one element is thin. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (SetCat‘𝑈)) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 ∃*𝑝 𝑝 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
Theorem | setc2othin 47764 | The category (SetCat‘2o) is thin. A special case of setcthin 47763. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (SetCat‘2o) ∈ ThinCat | ||
Theorem | thincsect 47765 | In a thin category, one morphism is a section of another iff they are pointing towards each other. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋)))) | ||
Theorem | thincsect2 47766 | In a thin category, 𝐹 is a section of 𝐺 iff 𝐺 is a section of 𝐹. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ 𝐺(𝑌𝑆𝑋)𝐹)) | ||
Theorem | thincinv 47767 | In a thin category, 𝐹 is an inverse of 𝐺 iff 𝐹 is a section of 𝐺 (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐹(𝑋𝑆𝑌)𝐺)) | ||
Theorem | thinciso 47768 | In a thin category, 𝐹:𝑋⟶𝑌 is an isomorphism iff there is a morphism from 𝑌 to 𝑋. (Contributed by Zhi Wang, 25-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ (𝑌𝐻𝑋) ≠ ∅)) | ||
Theorem | thinccic 47769 | In a thin category, two objects are isomorphic iff there are morphisms between them in both directions. (Contributed by Zhi Wang, 25-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ((𝑋𝐻𝑌) ≠ ∅ ∧ (𝑌𝐻𝑋) ≠ ∅))) | ||
Syntax | cprstc 47770 | Class function defining preordered sets as categories. |
class ProsetToCat | ||
Definition | df-prstc 47771 |
Definition of the function converting a preordered set to a category.
Justified by prsthinc 47762.
This definition is somewhat arbitrary. Example 3.3(4.d) of [Adamek] p. 24 demonstrates an alternate definition with pairwise disjoint hom-sets. The behavior of the function is defined entirely, up to isomorphism, by prstcnid 47774, prstchom 47785, and prstcthin 47784. Other important properties include prstcbas 47775, prstcleval 47776, prstcle 47778, prstcocval 47779, prstcoc 47781, prstchom2 47786, and prstcprs 47783. Use those instead. Note that the defining property prstchom 47785 is equivalent to prstchom2 47786 given prstcthin 47784. See thincn0eu 47740 for justification. "ProsetToCat" was taken instead of "ProsetCat" because the latter might mean the category of preordered sets (classes). However, "ProsetToCat" seems too long. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
⊢ ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) | ||
Theorem | prstcval 47772 | Lemma for prstcnidlem 47773 and prstcthin 47784. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 = ((𝐾 sSet 〈(Hom ‘ndx), ((le‘𝐾) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) | ||
Theorem | prstcnidlem 47773 | Lemma for prstcnid 47774 and prstchomval 47782. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (comp‘ndx) ⇒ ⊢ (𝜑 → (𝐸‘𝐶) = (𝐸‘(𝐾 sSet 〈(Hom ‘ndx), ((le‘𝐾) × {1o})〉))) | ||
Theorem | prstcnid 47774 | Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (comp‘ndx) & ⊢ (𝐸‘ndx) ≠ (Hom ‘ndx) ⇒ ⊢ (𝜑 → (𝐸‘𝐾) = (𝐸‘𝐶)) | ||
Theorem | prstcbas 47775 | The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
Theorem | prstcleval 47776 | Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → ≤ = (le‘𝐶)) | ||
Theorem | prstclevalOLD 47777 | Obsolete proof of prstcleval 47776 as of 12-Nov-2024. Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → ≤ = (le‘𝐶)) | ||
Theorem | prstcle 47778 | Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌)) | ||
Theorem | prstcocval 47779 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ⊥ = (oc‘𝐶)) | ||
Theorem | prstcocvalOLD 47780 | Obsolete proof of prstcocval 47779 as of 12-Nov-2024. Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ⊥ = (oc‘𝐶)) | ||
Theorem | prstcoc 47781 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋)) | ||
Theorem | prstchomval 47782 | Hom-sets of the constructed category which depend on an arbitrary definition. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶)) | ||
Theorem | prstcprs 47783 | The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
Theorem | prstcthin 47784 | The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
Theorem | prstchom 47785 |
Hom-sets of the constructed category are dependent on the preorder.
Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat. However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
Theorem | prstchom2 47786* |
Hom-sets of the constructed category are dependent on the preorder.
Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat ( see prstchom2ALT 47787). However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 21-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌))) | ||
Theorem | prstchom2ALT 47787* | Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 47771. See prstchom2 47786 for a version that does not depend on the definition. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌))) | ||
Theorem | postcpos 47788 | The converted category is a poset iff the original proset is a poset. (Contributed by Zhi Wang, 26-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset)) | ||
Theorem | postcposALT 47789 | Alternate proof for postcpos 47788. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset)) | ||
Theorem | postc 47790* | The converted category is a poset iff no distinct objects are isomorphic. (Contributed by Zhi Wang, 25-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝐶 ∈ Poset ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥( ≃𝑐 ‘𝐶)𝑦 → 𝑥 = 𝑦))) | ||
Syntax | cmndtc 47791 | Class function defining monoids as categories. |
class MndToCat | ||
Definition | df-mndtc 47792 |
Definition of the function converting a monoid to a category. Example
3.3(4.e) of [Adamek] p. 24.
The definition of the base set is arbitrary. The whole extensible structure becomes the object here (see mndtcbasval 47794), instead of just the base set, as is the case in Example 3.3(4.e) of [Adamek] p. 24. The resulting category is defined entirely, up to isomorphism, by mndtcbas 47795, mndtchom 47798, mndtcco 47799. Use those instead. See example 3.26(3) of [Adamek] p. 33 for more on isomorphism. "MndToCat" was taken instead of "MndCat" because the latter might mean the category of monoids. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
⊢ MndToCat = (𝑚 ∈ Mnd ↦ {〈(Base‘ndx), {𝑚}〉, 〈(Hom ‘ndx), {〈𝑚, 𝑚, (Base‘𝑚)〉}〉, 〈(comp‘ndx), {〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉}〉}) | ||
Theorem | mndtcval 47793 | Value of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), {𝑀}〉, 〈(Hom ‘ndx), {〈𝑀, 𝑀, (Base‘𝑀)〉}〉, 〈(comp‘ndx), {〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉}〉}) | ||
Theorem | mndtcbasval 47794 | The base set of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = {𝑀}) | ||
Theorem | mndtcbas 47795* | The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) ⇒ ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵) | ||
Theorem | mndtcob 47796 | Lemma for mndtchom 47798 and mndtcco 47799. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑀) | ||
Theorem | mndtcbas2 47797 | Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | mndtchom 47798 | The only hom-set of the category built from a monoid is the base set of the monoid. (Contributed by Zhi Wang, 22-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (Base‘𝑀)) | ||
Theorem | mndtcco 47799 | The composition of the category built from a monoid is the monoid operation. (Contributed by Zhi Wang, 22-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → · = (comp‘𝐶)) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉 · 𝑍) = (+g‘𝑀)) | ||
Theorem | mndtcco2 47800 | The composition of the category built from a monoid is the monoid operation. (Contributed by Zhi Wang, 22-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → ⚬ = (〈𝑋, 𝑌〉 · 𝑍)) ⇒ ⊢ (𝜑 → (𝐺 ⚬ 𝐹) = (𝐺(+g‘𝑀)𝐹)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |