Definition df-prstc 49711

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

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 49614), by prstcnid 49714, prstchom 49723, and prstcthin 49722. Other important properties include prstcbas 49715, prstcleval 49716, prstcle 49717, prstcocval 49718, prstcoc 49719, prstchom2 49724, and prstcprs 49721. Use those instead.

Note that the defining property prstchom 49723 is equivalent to prstchom2 49724 given prstcthin 49722. See thincn0eu 49592 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 49710	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18206	. . 3 class Proset
4	2	cv 1540	. . . . 5 class 𝑘
5		cnx 17111	. . . . . . 7 class ndx
6		chom 17179	. . . . . . 7 class Hom
7	5, 6	cfv 6489	. . . . . 6 class (Hom ‘ndx)
8		cple 17175	. . . . . . . 8 class le
9	4, 8	cfv 6489	. . . . . . 7 class (le‘𝑘)
10		c1o 8387	. . . . . . . 8 class 1o
11	10	csn 4577	. . . . . . 7 class {1o}
12	9, 11	cxp 5619	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4583	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17081	. . . . 5 class sSet
15	4, 13, 14	co 7355	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17180	. . . . . 6 class comp
17	5, 16	cfv 6489	. . . . 5 class (comp‘ndx)
18		c0 4282	. . . . 5 class ∅
19	17, 18	cop 4583	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7355	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5176	. 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  49712