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 46335.
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 46347, prstchom 46358, and prstcthin 46357. Other important properties include prstcbas 46348, prstcleval 46349, prstcle 46351, prstcocval 46352, prstcoc 46354, prstchom2 46359, and prstcprs 46356. Use those instead. Note that the defining property prstchom 46358 is equivalent to prstchom2 46359 given prstcthin 46357. See thincn0eu 46313 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 46343 | . 2 class ProsetToCat | |
2 | vk | . . 3 setvar 𝑘 | |
3 | cproset 18011 | . . 3 class Proset | |
4 | 2 | cv 1538 | . . . . 5 class 𝑘 |
5 | cnx 16894 | . . . . . . 7 class ndx | |
6 | chom 16973 | . . . . . . 7 class Hom | |
7 | 5, 6 | cfv 6433 | . . . . . 6 class (Hom ‘ndx) |
8 | cple 16969 | . . . . . . . 8 class le | |
9 | 4, 8 | cfv 6433 | . . . . . . 7 class (le‘𝑘) |
10 | c1o 8290 | . . . . . . . 8 class 1o | |
11 | 10 | csn 4561 | . . . . . . 7 class {1o} |
12 | 9, 11 | cxp 5587 | . . . . . 6 class ((le‘𝑘) × {1o}) |
13 | 7, 12 | cop 4567 | . . . . 5 class 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉 |
14 | csts 16864 | . . . . 5 class sSet | |
15 | 4, 13, 14 | co 7275 | . . . 4 class (𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) |
16 | cco 16974 | . . . . . 6 class comp | |
17 | 5, 16 | cfv 6433 | . . . . 5 class (comp‘ndx) |
18 | c0 4256 | . . . . 5 class ∅ | |
19 | 17, 18 | cop 4567 | . . . 4 class 〈(comp‘ndx), ∅〉 |
20 | 15, 19, 14 | co 7275 | . . 3 class ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉) |
21 | 2, 3, 20 | cmpt 5157 | . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) |
22 | 1, 21 | wceq 1539 | 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) |
Colors of variables: wff setvar class |
This definition is referenced by: prstcval 46345 |
Copyright terms: Public domain | W3C validator |