Definition df-prstc 49582

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

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 49485), by prstcnid 49585, prstchom 49594, and prstcthin 49593. Other important properties include prstcbas 49586, prstcleval 49587, prstcle 49588, prstcocval 49589, prstcoc 49590, prstchom2 49595, and prstcprs 49592. Use those instead.

Note that the defining property prstchom 49594 is equivalent to prstchom2 49595 given prstcthin 49593. See thincn0eu 49463 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 49581	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18193	. . 3 class Proset
4	2	cv 1540	. . . . 5 class 𝑘
5		cnx 17099	. . . . . . 7 class ndx
6		chom 17167	. . . . . . 7 class Hom
7	5, 6	cfv 6476	. . . . . 6 class (Hom ‘ndx)
8		cple 17163	. . . . . . . 8 class le
9	4, 8	cfv 6476	. . . . . . 7 class (le‘𝑘)
10		c1o 8373	. . . . . . . 8 class 1o
11	10	csn 4571	. . . . . . 7 class {1o}
12	9, 11	cxp 5609	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4577	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17069	. . . . 5 class sSet
15	4, 13, 14	co 7341	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17168	. . . . . 6 class comp
17	5, 16	cfv 6476	. . . . 5 class (comp‘ndx)
18		c0 4278	. . . . 5 class ∅
19	17, 18	cop 4577	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7341	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5167	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1541	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  49583