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 ( thincciso ), 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 ⊢ ProsetToCat = k ∈ Proset ⟼ k sSet Hom ⁡ ndx ≤ k × 1 𝑜 sSet comp ⁡ ndx ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprstc class ProsetToCat
1 vk setvar k
2 cproset class Proset
3 1 cv setvar k
4 csts class sSet
5 chom class Hom
6 cnx class ndx
7 6 5 cfv class Hom ⁡ ndx
8 cple class le
9 3 8 cfv class ≤ k
10 c1o class 1 𝑜
11 10 csn class 1 𝑜
12 9 11 cxp class ≤ k × 1 𝑜
13 7 12 cop class Hom ⁡ ndx ≤ k × 1 𝑜
14 3 13 4 co class k sSet Hom ⁡ ndx ≤ k × 1 𝑜
15 cco class comp
16 6 15 cfv class comp ⁡ ndx
17 c0 class ∅
18 16 17 cop class comp ⁡ ndx ∅
19 14 18 4 co class k sSet Hom ⁡ ndx ≤ k × 1 𝑜 sSet comp ⁡ ndx ∅
20 1 2 19 cmpt class k ∈ Proset ⟼ k sSet Hom ⁡ ndx ≤ k × 1 𝑜 sSet comp ⁡ ndx ∅
21 0 20 wceq wff ProsetToCat = k ∈ Proset ⟼ k sSet Hom ⁡ ndx ≤ k × 1 𝑜 sSet comp ⁡ ndx ∅