|   | Mathbox for Zhi Wang | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-prstc | Structured version Visualization version GIF version | ||
| Description: Definition of the
function converting a preordered set to a category.
       Justified by prsthinc 49111. 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 (thincciso 49102), by prstcnid 49155, prstchom 49166, and prstcthin 49165. Other important properties include prstcbas 49156, prstcleval 49157, prstcle 49159, prstcocval 49160, prstcoc 49162, prstchom2 49167, and prstcprs 49164. Use those instead. Note that the defining property prstchom 49166 is equivalent to prstchom2 49167 given prstcthin 49165. See thincn0eu 49080 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.) | 
| Ref | Expression | 
|---|---|
| df-prstc | ⊢ ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | cprstc 49151 | . 2 class ProsetToCat | |
| 2 | vk | . . 3 setvar 𝑘 | |
| 3 | cproset 18338 | . . 3 class Proset | |
| 4 | 2 | cv 1539 | . . . . 5 class 𝑘 | 
| 5 | cnx 17230 | . . . . . . 7 class ndx | |
| 6 | chom 17308 | . . . . . . 7 class Hom | |
| 7 | 5, 6 | cfv 6561 | . . . . . 6 class (Hom ‘ndx) | 
| 8 | cple 17304 | . . . . . . . 8 class le | |
| 9 | 4, 8 | cfv 6561 | . . . . . . 7 class (le‘𝑘) | 
| 10 | c1o 8499 | . . . . . . . 8 class 1o | |
| 11 | 10 | csn 4626 | . . . . . . 7 class {1o} | 
| 12 | 9, 11 | cxp 5683 | . . . . . 6 class ((le‘𝑘) × {1o}) | 
| 13 | 7, 12 | cop 4632 | . . . . 5 class 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉 | 
| 14 | csts 17200 | . . . . 5 class sSet | |
| 15 | 4, 13, 14 | co 7431 | . . . 4 class (𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) | 
| 16 | cco 17309 | . . . . . 6 class comp | |
| 17 | 5, 16 | cfv 6561 | . . . . 5 class (comp‘ndx) | 
| 18 | c0 4333 | . . . . 5 class ∅ | |
| 19 | 17, 18 | cop 4632 | . . . 4 class 〈(comp‘ndx), ∅〉 | 
| 20 | 15, 19, 14 | co 7431 | . . 3 class ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉) | 
| 21 | 2, 3, 20 | cmpt 5225 | . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) | 
| 22 | 1, 21 | wceq 1540 | 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: prstcval 49153 | 
| Copyright terms: Public domain | W3C validator |