Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prstc Structured version   Visualization version   GIF version

Definition df-prstc 45850
Description: Definition of the function converting a preordered set to a category. Justified by prsthinc 45846.

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 45853, prstchom 45862, and prstcthin 45861. Other important properties include prstcbas 45854, prstcleval 45855, prstcle 45856, prstcocval 45857, prstcoc 45858, prstchom2 45863, and prstcprs 45860. Use those instead.

Note that the defining property prstchom 45862 is equivalent to prstchom2 45863 given prstcthin 45861. See thincn0eu 45836 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.)

Assertion
Ref Expression
df-prstc ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

Detailed syntax breakdown of Definition df-prstc
StepHypRef Expression
1 cprstc 45849 . 2 class ProsetToCat
2 vk . . 3 setvar 𝑘
3 cproset 17664 . . 3 class Proset
42cv 1541 . . . . 5 class 𝑘
5 cnx 16595 . . . . . . 7 class ndx
6 chom 16691 . . . . . . 7 class Hom
75, 6cfv 6349 . . . . . 6 class (Hom ‘ndx)
8 cple 16687 . . . . . . . 8 class le
94, 8cfv 6349 . . . . . . 7 class (le‘𝑘)
10 c1o 8136 . . . . . . . 8 class 1o
1110csn 4526 . . . . . . 7 class {1o}
129, 11cxp 5533 . . . . . 6 class ((le‘𝑘) × {1o})
137, 12cop 4532 . . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14 csts 16596 . . . . 5 class sSet
154, 13, 14co 7182 . . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16 cco 16692 . . . . . 6 class comp
175, 16cfv 6349 . . . . 5 class (comp‘ndx)
18 c0 4221 . . . . 5 class
1917, 18cop 4532 . . . 4 class ⟨(comp‘ndx), ∅⟩
2015, 19, 14co 7182 . . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
212, 3, 20cmpt 5120 . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
221, 21wceq 1542 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Colors of variables: wff setvar class
This definition is referenced by:  prstcval  45851
  Copyright terms: Public domain W3C validator