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 45951.
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 45963, prstchom 45972, and prstcthin 45971. Other important properties include prstcbas 45964, prstcleval 45965, prstcle 45966, prstcocval 45967, prstcoc 45968, prstchom2 45973, and prstcprs 45970. Use those instead. Note that the defining property prstchom 45972 is equivalent to prstchom2 45973 given prstcthin 45971. See thincn0eu 45929 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 45959 | . 2 class ProsetToCat | |
2 | vk | . . 3 setvar 𝑘 | |
3 | cproset 17754 | . . 3 class Proset | |
4 | 2 | cv 1542 | . . . . 5 class 𝑘 |
5 | cnx 16663 | . . . . . . 7 class ndx | |
6 | chom 16760 | . . . . . . 7 class Hom | |
7 | 5, 6 | cfv 6358 | . . . . . 6 class (Hom ‘ndx) |
8 | cple 16756 | . . . . . . . 8 class le | |
9 | 4, 8 | cfv 6358 | . . . . . . 7 class (le‘𝑘) |
10 | c1o 8173 | . . . . . . . 8 class 1o | |
11 | 10 | csn 4527 | . . . . . . 7 class {1o} |
12 | 9, 11 | cxp 5534 | . . . . . 6 class ((le‘𝑘) × {1o}) |
13 | 7, 12 | cop 4533 | . . . . 5 class 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉 |
14 | csts 16664 | . . . . 5 class sSet | |
15 | 4, 13, 14 | co 7191 | . . . 4 class (𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) |
16 | cco 16761 | . . . . . 6 class comp | |
17 | 5, 16 | cfv 6358 | . . . . 5 class (comp‘ndx) |
18 | c0 4223 | . . . . 5 class ∅ | |
19 | 17, 18 | cop 4533 | . . . 4 class 〈(comp‘ndx), ∅〉 |
20 | 15, 19, 14 | co 7191 | . . 3 class ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉) |
21 | 2, 3, 20 | cmpt 5120 | . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) |
22 | 1, 21 | wceq 1543 | 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) |
Colors of variables: wff setvar class |
This definition is referenced by: prstcval 45961 |
Copyright terms: Public domain | W3C validator |