Definition df-prstc 49906

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

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 49809), by prstcnid 49909, prstchom 49918, and prstcthin 49917. Other important properties include prstcbas 49910, prstcleval 49911, prstcle 49912, prstcocval 49913, prstcoc 49914, prstchom2 49919, and prstcprs 49916. Use those instead.

Note that the defining property prstchom 49918 is equivalent to prstchom2 49919 given prstcthin 49917. See thincn0eu 49787 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.)

Assertion

Ref	Expression
df-prstc	⊢ ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

Detailed syntax breakdown of Definition df-prstc

Step	Hyp	Ref	Expression
1		cprstc 49905	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18227	. . 3 class Proset
4	2	cv 1541	. . . . 5 class 𝑘
5		cnx 17132	. . . . . . 7 class ndx
6		chom 17200	. . . . . . 7 class Hom
7	5, 6	cfv 6500	. . . . . 6 class (Hom ‘ndx)
8		cple 17196	. . . . . . . 8 class le
9	4, 8	cfv 6500	. . . . . . 7 class (le‘𝑘)
10		c1o 8400	. . . . . . . 8 class 1o
11	10	csn 4582	. . . . . . 7 class {1o}
12	9, 11	cxp 5630	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4588	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17102	. . . . 5 class sSet
15	4, 13, 14	co 7368	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17201	. . . . . 6 class comp
17	5, 16	cfv 6500	. . . . 5 class (comp‘ndx)
18		c0 4287	. . . . 5 class ∅
19	17, 18	cop 4588	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7368	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5181	. 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), ∅⟩))

This definition is referenced by:  prstcval  49907