![]() |
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 48060.
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 48072, prstchom 48083, and prstcthin 48082. Other important properties include prstcbas 48073, prstcleval 48074, prstcle 48076, prstcocval 48077, prstcoc 48079, prstchom2 48084, and prstcprs 48081. Use those instead. Note that the defining property prstchom 48083 is equivalent to prstchom2 48084 given prstcthin 48082. See thincn0eu 48038 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 48068 | . 2 class ProsetToCat | |
2 | vk | . . 3 setvar 𝑘 | |
3 | cproset 18285 | . . 3 class Proset | |
4 | 2 | cv 1533 | . . . . 5 class 𝑘 |
5 | cnx 17162 | . . . . . . 7 class ndx | |
6 | chom 17244 | . . . . . . 7 class Hom | |
7 | 5, 6 | cfv 6548 | . . . . . 6 class (Hom ‘ndx) |
8 | cple 17240 | . . . . . . . 8 class le | |
9 | 4, 8 | cfv 6548 | . . . . . . 7 class (le‘𝑘) |
10 | c1o 8480 | . . . . . . . 8 class 1o | |
11 | 10 | csn 4629 | . . . . . . 7 class {1o} |
12 | 9, 11 | cxp 5676 | . . . . . 6 class ((le‘𝑘) × {1o}) |
13 | 7, 12 | cop 4635 | . . . . 5 class 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉 |
14 | csts 17132 | . . . . 5 class sSet | |
15 | 4, 13, 14 | co 7420 | . . . 4 class (𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) |
16 | cco 17245 | . . . . . 6 class comp | |
17 | 5, 16 | cfv 6548 | . . . . 5 class (comp‘ndx) |
18 | c0 4323 | . . . . 5 class ∅ | |
19 | 17, 18 | cop 4635 | . . . 4 class 〈(comp‘ndx), ∅〉 |
20 | 15, 19, 14 | co 7420 | . . 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 1534 | 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) sSet 〈(comp‘ndx), ∅〉)) |
Colors of variables: wff setvar class |
This definition is referenced by: prstcval 48070 |
Copyright terms: Public domain | W3C validator |