![]() |
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 47763.
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 47775, prstchom 47786, and prstcthin 47785. Other important properties include prstcbas 47776, prstcleval 47777, prstcle 47779, prstcocval 47780, prstcoc 47782, prstchom2 47787, and prstcprs 47784. Use those instead. Note that the defining property prstchom 47786 is equivalent to prstchom2 47787 given prstcthin 47785. See thincn0eu 47741 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 47771 | . 2 class ProsetToCat | |
2 | vk | . . 3 setvar 𝑘 | |
3 | cproset 18251 | . . 3 class Proset | |
4 | 2 | cv 1539 | . . . . 5 class 𝑘 |
5 | cnx 17131 | . . . . . . 7 class ndx | |
6 | chom 17213 | . . . . . . 7 class Hom | |
7 | 5, 6 | cfv 6544 | . . . . . 6 class (Hom ‘ndx) |
8 | cple 17209 | . . . . . . . 8 class le | |
9 | 4, 8 | cfv 6544 | . . . . . . 7 class (le‘𝑘) |
10 | c1o 8462 | . . . . . . . 8 class 1o | |
11 | 10 | csn 4629 | . . . . . . 7 class {1o} |
12 | 9, 11 | cxp 5675 | . . . . . 6 class ((le‘𝑘) × {1o}) |
13 | 7, 12 | cop 4635 | . . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩ |
14 | csts 17101 | . . . . 5 class sSet | |
15 | 4, 13, 14 | co 7412 | . . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) |
16 | cco 17214 | . . . . . 6 class comp | |
17 | 5, 16 | cfv 6544 | . . . . 5 class (comp‘ndx) |
18 | c0 4323 | . . . . 5 class ∅ | |
19 | 17, 18 | cop 4635 | . . . 4 class ⟨(comp‘ndx), ∅⟩ |
20 | 15, 19, 14 | co 7412 | . . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩) |
21 | 2, 3, 20 | cmpt 5232 | . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)) |
22 | 1, 21 | wceq 1540 | 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)) |
Colors of variables: wff setvar class |
This definition is referenced by: prstcval 47773 |
Copyright terms: Public domain | W3C validator |