![]() |
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 48855.
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 48867, prstchom 48878, and prstcthin 48877. Other important properties include prstcbas 48868, prstcleval 48869, prstcle 48871, prstcocval 48872, prstcoc 48874, prstchom2 48879, and prstcprs 48876. Use those instead. Note that the defining property prstchom 48878 is equivalent to prstchom2 48879 given prstcthin 48877. See thincn0eu 48832 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 48863 | . 2 class ProsetToCat | |
2 | vk | . . 3 setvar 𝑘 | |
3 | cproset 18350 | . . 3 class Proset | |
4 | 2 | cv 1536 | . . . . 5 class 𝑘 |
5 | cnx 17227 | . . . . . . 7 class ndx | |
6 | chom 17309 | . . . . . . 7 class Hom | |
7 | 5, 6 | cfv 6563 | . . . . . 6 class (Hom ‘ndx) |
8 | cple 17305 | . . . . . . . 8 class le | |
9 | 4, 8 | cfv 6563 | . . . . . . 7 class (le‘𝑘) |
10 | c1o 8498 | . . . . . . . 8 class 1o | |
11 | 10 | csn 4631 | . . . . . . 7 class {1o} |
12 | 9, 11 | cxp 5687 | . . . . . 6 class ((le‘𝑘) × {1o}) |
13 | 7, 12 | cop 4637 | . . . . 5 class 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉 |
14 | csts 17197 | . . . . 5 class sSet | |
15 | 4, 13, 14 | co 7431 | . . . 4 class (𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) |
16 | cco 17310 | . . . . . 6 class comp | |
17 | 5, 16 | cfv 6563 | . . . . 5 class (comp‘ndx) |
18 | c0 4339 | . . . . 5 class ∅ | |
19 | 17, 18 | cop 4637 | . . . 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 5231 | . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) |
22 | 1, 21 | wceq 1537 | 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) |
Colors of variables: wff setvar class |
This definition is referenced by: prstcval 48865 |
Copyright terms: Public domain | W3C validator |