![]() |
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 47164.
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 47176, prstchom 47187, and prstcthin 47186. Other important properties include prstcbas 47177, prstcleval 47178, prstcle 47180, prstcocval 47181, prstcoc 47183, prstchom2 47188, and prstcprs 47185. Use those instead. Note that the defining property prstchom 47187 is equivalent to prstchom2 47188 given prstcthin 47186. See thincn0eu 47142 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 47172 | . 2 class ProsetToCat | |
2 | vk | . . 3 setvar 𝑘 | |
3 | cproset 18190 | . . 3 class Proset | |
4 | 2 | cv 1541 | . . . . 5 class 𝑘 |
5 | cnx 17073 | . . . . . . 7 class ndx | |
6 | chom 17152 | . . . . . . 7 class Hom | |
7 | 5, 6 | cfv 6500 | . . . . . 6 class (Hom ‘ndx) |
8 | cple 17148 | . . . . . . . 8 class le | |
9 | 4, 8 | cfv 6500 | . . . . . . 7 class (le‘𝑘) |
10 | c1o 8409 | . . . . . . . 8 class 1o | |
11 | 10 | csn 4590 | . . . . . . 7 class {1o} |
12 | 9, 11 | cxp 5635 | . . . . . 6 class ((le‘𝑘) × {1o}) |
13 | 7, 12 | cop 4596 | . . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩ |
14 | csts 17043 | . . . . 5 class sSet | |
15 | 4, 13, 14 | co 7361 | . . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) |
16 | cco 17153 | . . . . . 6 class comp | |
17 | 5, 16 | cfv 6500 | . . . . 5 class (comp‘ndx) |
18 | c0 4286 | . . . . 5 class ∅ | |
19 | 17, 18 | cop 4596 | . . . 4 class ⟨(comp‘ndx), ∅⟩ |
20 | 15, 19, 14 | co 7361 | . . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩) |
21 | 2, 3, 20 | cmpt 5192 | . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)) |
22 | 1, 21 | wceq 1542 | 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)) |
Colors of variables: wff setvar class |
This definition is referenced by: prstcval 47174 |
Copyright terms: Public domain | W3C validator |