![]() |
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 47761.
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 47773, prstchom 47784, and prstcthin 47783. Other important properties include prstcbas 47774, prstcleval 47775, prstcle 47777, prstcocval 47778, prstcoc 47780, prstchom2 47785, and prstcprs 47782. Use those instead. Note that the defining property prstchom 47784 is equivalent to prstchom2 47785 given prstcthin 47783. See thincn0eu 47739 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 47769 | . 2 class ProsetToCat | |
2 | vk | . . 3 setvar 𝑘 | |
3 | cproset 18250 | . . 3 class Proset | |
4 | 2 | cv 1538 | . . . . 5 class 𝑘 |
5 | cnx 17130 | . . . . . . 7 class ndx | |
6 | chom 17212 | . . . . . . 7 class Hom | |
7 | 5, 6 | cfv 6542 | . . . . . 6 class (Hom ‘ndx) |
8 | cple 17208 | . . . . . . . 8 class le | |
9 | 4, 8 | cfv 6542 | . . . . . . 7 class (le‘𝑘) |
10 | c1o 8461 | . . . . . . . 8 class 1o | |
11 | 10 | csn 4627 | . . . . . . 7 class {1o} |
12 | 9, 11 | cxp 5673 | . . . . . 6 class ((le‘𝑘) × {1o}) |
13 | 7, 12 | cop 4633 | . . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩ |
14 | csts 17100 | . . . . 5 class sSet | |
15 | 4, 13, 14 | co 7411 | . . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) |
16 | cco 17213 | . . . . . 6 class comp | |
17 | 5, 16 | cfv 6542 | . . . . 5 class (comp‘ndx) |
18 | c0 4321 | . . . . 5 class ∅ | |
19 | 17, 18 | cop 4633 | . . . 4 class ⟨(comp‘ndx), ∅⟩ |
20 | 15, 19, 14 | co 7411 | . . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩) |
21 | 2, 3, 20 | cmpt 5230 | . 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 47771 |
Copyright terms: Public domain | W3C validator |