Definition df-prstc 49394

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

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 49306), by prstcnid 49397, prstchom 49406, and prstcthin 49405. Other important properties include prstcbas 49398, prstcleval 49399, prstcle 49400, prstcocval 49401, prstcoc 49402, prstchom2 49407, and prstcprs 49404. Use those instead.

Note that the defining property prstchom 49406 is equivalent to prstchom2 49407 given prstcthin 49405. See thincn0eu 49284 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 49393	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18309	. . 3 class Proset
4	2	cv 1539	. . . . 5 class 𝑘
5		cnx 17217	. . . . . . 7 class ndx
6		chom 17287	. . . . . . 7 class Hom
7	5, 6	cfv 6536	. . . . . 6 class (Hom ‘ndx)
8		cple 17283	. . . . . . . 8 class le
9	4, 8	cfv 6536	. . . . . . 7 class (le‘𝑘)
10		c1o 8478	. . . . . . . 8 class 1o
11	10	csn 4606	. . . . . . 7 class {1o}
12	9, 11	cxp 5657	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4612	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17187	. . . . 5 class sSet
15	4, 13, 14	co 7410	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17288	. . . . . 6 class comp
17	5, 16	cfv 6536	. . . . 5 class (comp‘ndx)
18		c0 4313	. . . . 5 class ∅
19	17, 18	cop 4612	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7410	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5206	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1540	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  49395