Definition df-prstc 49795

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

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 49698), by prstcnid 49798, prstchom 49807, and prstcthin 49806. Other important properties include prstcbas 49799, prstcleval 49800, prstcle 49801, prstcocval 49802, prstcoc 49803, prstchom2 49808, and prstcprs 49805. Use those instead.

Note that the defining property prstchom 49807 is equivalent to prstchom2 49808 given prstcthin 49806. See thincn0eu 49676 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 49794	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18215	. . 3 class Proset
4	2	cv 1540	. . . . 5 class 𝑘
5		cnx 17120	. . . . . . 7 class ndx
6		chom 17188	. . . . . . 7 class Hom
7	5, 6	cfv 6492	. . . . . 6 class (Hom ‘ndx)
8		cple 17184	. . . . . . . 8 class le
9	4, 8	cfv 6492	. . . . . . 7 class (le‘𝑘)
10		c1o 8390	. . . . . . . 8 class 1o
11	10	csn 4580	. . . . . . 7 class {1o}
12	9, 11	cxp 5622	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4586	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17090	. . . . 5 class sSet
15	4, 13, 14	co 7358	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17189	. . . . . 6 class comp
17	5, 16	cfv 6492	. . . . 5 class (comp‘ndx)
18		c0 4285	. . . . 5 class ∅
19	17, 18	cop 4586	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7358	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5179	. 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  49796