Definition df-prstc 50385

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

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 50288), by prstcnid 50388, prstchom 50397, and prstcthin 50396. Other important properties include prstcbas 50389, prstcleval 50390, prstcle 50391, prstcocval 50392, prstcoc 50393, prstchom2 50398, and prstcprs 50395. Use those instead.

Note that the defining property prstchom 50397 is equivalent to prstchom2 50398 given prstcthin 50396. See thincn0eu 50266 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 50384	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18370	. . 3 class Proset
4	2	cv 1569	. . . . 5 class 𝑘
5		cnx 17275	. . . . . . 7 class ndx
6		chom 17343	. . . . . . 7 class Hom
7	5, 6	cfv 6540	. . . . . 6 class (Hom ‘ndx)
8		cple 17339	. . . . . . . 8 class le
9	4, 8	cfv 6540	. . . . . . 7 class (le‘𝑘)
10		c1o 8452	. . . . . . . 8 class 1o
11	10	csn 4591	. . . . . . 7 class {1o}
12	9, 11	cxp 5661	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4597	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17245	. . . . 5 class sSet
15	4, 13, 14	co 7419	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17344	. . . . . 6 class comp
17	5, 16	cfv 6540	. . . . 5 class (comp‘ndx)
18		c0 4286	. . . . 5 class ∅
19	17, 18	cop 4597	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7419	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5194	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1570	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is used by:  prstcval  50386