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 45846.
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 45853, prstchom 45862, and prstcthin 45861. Other important properties include prstcbas 45854, prstcleval 45855, prstcle 45856, prstcocval 45857, prstcoc 45858, prstchom2 45863, and prstcprs 45860. Use those instead. Note that the defining property prstchom 45862 is equivalent to prstchom2 45863 given prstcthin 45861. See thincn0eu 45836 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 45849 | . 2 class ProsetToCat | |
2 | vk | . . 3 setvar 𝑘 | |
3 | cproset 17664 | . . 3 class Proset | |
4 | 2 | cv 1541 | . . . . 5 class 𝑘 |
5 | cnx 16595 | . . . . . . 7 class ndx | |
6 | chom 16691 | . . . . . . 7 class Hom | |
7 | 5, 6 | cfv 6349 | . . . . . 6 class (Hom ‘ndx) |
8 | cple 16687 | . . . . . . . 8 class le | |
9 | 4, 8 | cfv 6349 | . . . . . . 7 class (le‘𝑘) |
10 | c1o 8136 | . . . . . . . 8 class 1o | |
11 | 10 | csn 4526 | . . . . . . 7 class {1o} |
12 | 9, 11 | cxp 5533 | . . . . . 6 class ((le‘𝑘) × {1o}) |
13 | 7, 12 | cop 4532 | . . . . 5 class 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉 |
14 | csts 16596 | . . . . 5 class sSet | |
15 | 4, 13, 14 | co 7182 | . . . 4 class (𝑘 sSet 〈(Hom ‘ndx), ((le‘𝑘) × {1o})〉) |
16 | cco 16692 | . . . . . 6 class comp | |
17 | 5, 16 | cfv 6349 | . . . . 5 class (comp‘ndx) |
18 | c0 4221 | . . . . 5 class ∅ | |
19 | 17, 18 | cop 4532 | . . . 4 class 〈(comp‘ndx), ∅〉 |
20 | 15, 19, 14 | co 7182 | . . 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 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 45851 |
Copyright terms: Public domain | W3C validator |