![]() |
Metamath
Proof Explorer Theorem List (p. 479 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ipolub 47801* | The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18369 is in quantified form. mrelatlub 18517 could potentially be shortened using this. See mrelatlubALT 47808. (Contributed by Zhi Wang, 28-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
Theorem | ipoglblem 47802* | Lemma for ipoglbdm 47803 and ipoglb 47804. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋)))) | ||
Theorem | ipoglbdm 47803* | The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹)) | ||
Theorem | ipoglb 47804* | The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18370 is in quantified form. mrelatglb 18515 could potentially be shortened using this. See mrelatglbALT 47809. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇) | ||
Theorem | ipolub0 47805 | The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹) | ||
Theorem | ipolub00 47806 | 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 47807 | The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹) | ||
Theorem | mrelatlubALT 47808 | 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 47809 | 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 47810 | A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
Theorem | topclat 47811 | A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat) | ||
Theorem | toplatglb0 47812 | The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽) | ||
Theorem | toplatlub 47813 | Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑆 ⊆ 𝐽) & ⊢ 𝑈 = (lub‘𝐼) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆) | ||
Theorem | toplatglb 47814 | 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 47815 | Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∨ = (join‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵)) | ||
Theorem | toplatmeet 47816 | Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∧ = (meet‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵)) | ||
Theorem | topdlat 47817 | A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat) | ||
Theorem | catprslem 47818* | Lemma for catprs 47819. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
Theorem | catprs 47819* | A preorder can be extracted from a category. See catprs2 47820 for more details. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
Theorem | catprs2 47820* | 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 47821 and catprsc2 47822 for constructions satisfying the hypothesis "catprs.1". See catprs 47819 for a more primitive version. See prsthinc 47862 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
Theorem | catprsc 47821* | A construction of the preorder induced by a category. See catprs2 47820 for details. See also catprsc2 47822 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → ≤ = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
Theorem | catprsc2 47822* | An alternate construction of the preorder induced by a category. See catprs2 47820 for details. See also catprsc 47821 for a different construction. The two constructions are different because df-cat 17611 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (𝜑 → ≤ = {〈𝑥, 𝑦〉 ∣ (𝑥𝐻𝑦) ≠ ∅}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
Theorem | endmndlem 47823 | A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 47892 for converting a monoid to a category. Lemma for bj-endmnd 36689. (Contributed by Zhi Wang, 25-Sep-2024.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀)) & ⊢ (𝜑 → (〈𝑋, 𝑋〉 · 𝑋) = (+g‘𝑀)) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mnd) | ||
Theorem | idmon 47824 | 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 47825 | 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 47826* | 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 47827 | Extend class notation with the class of thin categories. |
class ThinCat | ||
Definition | df-thinc 47828* | 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 47829* | The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))) | ||
Theorem | isthinc2 47830* | 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 47831* | 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 47832 | A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝐶 ∈ ThinCat → 𝐶 ∈ Cat) | ||
Theorem | thinccd 47833 | A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
Theorem | thincssc 47834 | A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ ThinCat ⊆ Cat | ||
Theorem | isthincd2lem1 47835* | Lemma for isthincd2 47846 and thincmo2 47836. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | thincmo2 47836 | Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | thincmo 47837* | There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
Theorem | thincmoALT 47838* | Alternate proof for thincmo 47837. (Contributed by Zhi Wang, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
Theorem | thincmod 47839* | At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) ⇒ ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌)) | ||
Theorem | thincn0eu 47840* | 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 47841 | 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 47842 | In a thin category, all morphisms are monomorphisms. The converse does not hold. See grptcmon 47904. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑀 = (Mono‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌)) | ||
Theorem | thincepi 47843 | In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi 47905. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐸 = (Epi‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌)) | ||
Theorem | isthincd2lem2 47844* | Lemma for isthincd2 47846. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)) | ||
Theorem | isthincd 47845* | The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
Theorem | isthincd2 47846* | 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 47847 | The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat) | ||
Theorem | subthinc 47848 | A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ ThinCat) ⇒ ⊢ (𝜑 → 𝐷 ∈ ThinCat) | ||
Theorem | functhinclem1 47849* | Lemma for functhinc 47853. 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 47850* | Lemma for functhinc 47853. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅)) ⇒ ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅)) | ||
Theorem | functhinclem3 47851* | Lemma for functhinc 47853. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))) & ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅)) & ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
Theorem | functhinclem4 47852* | Lemma for functhinc 47853. 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 47853* | 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 47820). (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ ThinCat) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅)) ⇒ ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾)) | ||
Theorem | fullthinc 47854* | 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 47855 | 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 47856 | A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.) |
⊢ (𝜑 → 𝐶 ∈ ThinCat) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) | ||
Theorem | thincciso 47857* | 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 47858 | Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat) | ||
Theorem | 0thinc 47859 | The empty category (see 0cat 17632) is thin. (Contributed by Zhi Wang, 17-Sep-2024.) |
⊢ ∅ ∈ ThinCat | ||
Theorem | indthinc 47860* | 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 47862, 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 47861* | An alternate proof for indthinc 47860 assuming more axioms including ax-pow 5353 and ax-un 7718. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶)) & ⊢ (𝜑 → ∅ = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) | ||
Theorem | prsthinc 47862* | 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 47819 and catprs2 47820 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 47863* | 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 47864 | The category (SetCat‘2o) is thin. A special case of setcthin 47863. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (SetCat‘2o) ∈ ThinCat | ||
Theorem | thincsect 47865 | 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 47866 | 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 47867 | 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 47868 | 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 47869 | 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 47870 | Class function defining preordered sets as categories. |
class ProsetToCat | ||
Definition | df-prstc 47871 |
Definition of the function converting a preordered set to a category.
Justified by prsthinc 47862.
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 47874, prstchom 47885, and prstcthin 47884. Other important properties include prstcbas 47875, prstcleval 47876, prstcle 47878, prstcocval 47879, prstcoc 47881, prstchom2 47886, and prstcprs 47883. Use those instead. Note that the defining property prstchom 47885 is equivalent to prstchom2 47886 given prstcthin 47884. See thincn0eu 47840 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 47872 | Lemma for prstcnidlem 47873 and prstcthin 47884. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 = ((𝐾 sSet 〈(Hom ‘ndx), ((le‘𝐾) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) | ||
Theorem | prstcnidlem 47873 | Lemma for prstcnid 47874 and prstchomval 47882. (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 47874 | 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 47875 | The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
Theorem | prstcleval 47876 | 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 47877 | Obsolete proof of prstcleval 47876 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 47878 | Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ≤ = (le‘𝐾)) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌)) | ||
Theorem | prstcocval 47879 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ⊥ = (oc‘𝐶)) | ||
Theorem | prstcocvalOLD 47880 | Obsolete proof of prstcocval 47879 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 47881 | Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) & ⊢ (𝜑 → ⊥ = (oc‘𝐾)) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋)) | ||
Theorem | prstchomval 47882 | 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 47883 | The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
Theorem | prstcthin 47884 | The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → 𝐶 ∈ ThinCat) | ||
Theorem | prstchom 47885 |
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 47886* |
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 47887). 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 47887* | Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 47871. See prstchom2 47886 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 47888 | 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 47889 | Alternate proof for postcpos 47888. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset)) | ||
Theorem | postc 47890* | 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 47891 | Class function defining monoids as categories. |
class MndToCat | ||
Definition | df-mndtc 47892 |
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 47894), 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 47895, mndtchom 47898, mndtcco 47899. 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 47893 | 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 47894 | 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 47895* | The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) ⇒ ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵) | ||
Theorem | mndtcob 47896 | Lemma for mndtchom 47898 and mndtcco 47899. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑀) | ||
Theorem | mndtcbas2 47897 | Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | mndtchom 47898 | 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 47899 | 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 47900 | 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 > |