Metamath Proof Explorer


Definition df-prstc

Description: Definition of the function converting a preordered set to a category. Justified by prsthinc .

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 , prstchom , and prstcthin . Other important properties include prstcbas , prstcleval , prstcle , prstcocval , prstcoc , prstchom2 , and prstcprs . Use those instead.

Note that the defining property prstchom is equivalent to prstchom2 given prstcthin . See thincn0eu 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
Assertion df-prstc Could not format assertion : No typesetting found for |- ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprstc Could not format ProsetToCat : No typesetting found for class ProsetToCat with typecode class
1 vk setvark
2 cproset classProset
3 1 cv setvark
4 csts classsSet
5 chom classHom
6 cnx classndx
7 6 5 cfv classHomndx
8 cple classle
9 3 8 cfv classk
10 c1o class1𝑜
11 10 csn class1𝑜
12 9 11 cxp classk×1𝑜
13 7 12 cop classHomndxk×1𝑜
14 3 13 4 co classksSetHomndxk×1𝑜
15 cco classcomp
16 6 15 cfv classcompndx
17 c0 class
18 16 17 cop classcompndx
19 14 18 4 co classksSetHomndxk×1𝑜sSetcompndx
20 1 2 19 cmpt classkProsetksSetHomndxk×1𝑜sSetcompndx
21 0 20 wceq Could not format ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) : No typesetting found for wff ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode wff