Definition df-prstc 46344

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

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 46347, prstchom 46358, and prstcthin 46357. Other important properties include prstcbas 46348, prstcleval 46349, prstcle 46351, prstcocval 46352, prstcoc 46354, prstchom2 46359, and prstcprs 46356. Use those instead.

Note that the defining property prstchom 46358 is equivalent to prstchom2 46359 given prstcthin 46357. See thincn0eu 46313 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 46343	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18011	. . 3 class Proset
4	2	cv 1538	. . . . 5 class 𝑘
5		cnx 16894	. . . . . . 7 class ndx
6		chom 16973	. . . . . . 7 class Hom
7	5, 6	cfv 6433	. . . . . 6 class (Hom ‘ndx)
8		cple 16969	. . . . . . . 8 class le
9	4, 8	cfv 6433	. . . . . . 7 class (le‘𝑘)
10		c1o 8290	. . . . . . . 8 class 1o
11	10	csn 4561	. . . . . . 7 class {1o}
12	9, 11	cxp 5587	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4567	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 16864	. . . . 5 class sSet
15	4, 13, 14	co 7275	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 16974	. . . . . 6 class comp
17	5, 16	cfv 6433	. . . . 5 class (comp‘ndx)
18		c0 4256	. . . . 5 class ∅
19	17, 18	cop 4567	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7275	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5157	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1539	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  46345